:: AFF_4 semantic presentation

E1: for b1 being AffinSpace
for b2 being Subset of b1
for b3 being set holds
( b3 in b2 implies b3 is Element of b1 )
;

theorem E2: :: AFF_4:1
for b1 being AffinSpace
for b2, b3, b4, b5 being Element of b1 holds
not ( ( LIN b2,b3,b4 or LIN b2,b4,b3 ) & b2 <> b3 & for b6 being Element of b1 holds
not ( LIN b2,b5,b6 & b3,b5 // b4,b6 ) )
proof
let c1 be AffinSpace;
let c2, c3, c4, c5 be Element of c1;
assume that E3: ( LIN c2,c3,c4 or LIN c2,c4,c3 )
and E4: c2 <> c3 ;
c3,c2 // c2,c4
proof
LIN c2,c3,c4 by E3, AFF_1:15;
then c2,c3 // c2,c4 by AFF_1:def 1;
hence c3,c2 // c2,c4 by AFF_1:13;
end;
then consider c6 being Element of c1 such that
E5: c5,c2 // c2,c6
and E6: c5,c3 // c4,c6 by E4, DIRAF:47;
c2,c5 // c2,c6 by E5, AFF_1:13;
then ( LIN c2,c5,c6 & c3,c5 // c4,c6 ) by E6, AFF_1:13, AFF_1:def 1;
hence ex b1 being Element of c1 st
( LIN c2,c5,b1 & c3,c5 // c4,b1 ) ;
end;

theorem E3: :: AFF_4:2
for b1 being AffinSpace
for b2, b3 being Element of b1
for b4 being Subset of b1 holds
( ( b2 in b4 ) implies ( ( not b2,b3 // b4 & not b3,b2 // b4 ) or b3 in b4 ) )
proof
let c1 be AffinSpace;
let c2, c3 be Element of c1;
let c4 be Subset of c1;
assume that E4: ( c2,c3 // c4 or c3,c2 // c4 )
and E5: c2 in c4 ;
( c2,c3 // c4 & c4 is is_line ) by E4, AFF_1:40, AFF_1:48;
hence c3 in c4 by E5, AFF_1:37;
end;

theorem E4: :: AFF_4:3
for b1 being AffinSpace
for b2, b3 being Element of b1
for b4, b5 being Subset of b1 holds
( ( ) implies ( ( not b2,b3 // b4 & not b3,b2 // b4 ) or ( not b4 // b5 & not b5 // b4 ) or ( b2,b3 // b5 & b3,b2 // b5 ) ) )
proof
let c1 be AffinSpace;
let c2, c3 be Element of c1;
let c4, c5 be Subset of c1;
assume that E5: ( c2,c3 // c4 or c3,c2 // c4 )
and E6: ( c4 // c5 or c5 // c4 ) ;
( c2,c3 // c4 & c4 // c5 ) by E5, E6, AFF_1:48;
hence c2,c3 // c5 by AFF_1:57;
hence c3,c2 // c5 by AFF_1:48;
end;

theorem E5: :: AFF_4:4
for b1 being AffinSpace
for b2, b3, b4, b5 being Element of b1
for b6 being Subset of b1 holds
( ( ) implies ( ( not b2,b3 // b6 & not b3,b2 // b6 ) or ( not b2,b3 // b4,b5 & not b4,b5 // b2,b3 ) or not b2 <> b3 or ( b4,b5 // b6 & b5,b4 // b6 ) ) )
proof
let c1 be AffinSpace;
let c2, c3, c4, c5 be Element of c1;
let c6 be Subset of c1;
assume that E6: ( c2,c3 // c6 or c3,c2 // c6 )
and E7: ( c2,c3 // c4,c5 or c4,c5 // c2,c3 )
and E8: c2 <> c3 ;
( c2,c3 // c6 & c2,c3 // c4,c5 ) by E6, E7, AFF_1:13, AFF_1:48;
hence c4,c5 // c6 by E8, AFF_1:46;
hence c5,c4 // c6 by AFF_1:48;
end;

theorem :: AFF_4:5
for b1 being AffinSpace
for b2, b3 being Element of b1
for b4, b5 being Subset of b1 holds
( ( ) implies ( ( not b2,b3 // b4 & not b3,b2 // b4 ) or ( not b2,b3 // b5 & not b3,b2 // b5 ) or not b2 <> b3 or ( b4 // b5 & b5 // b4 ) ) )
proof
let c1 be AffinSpace;
let c2, c3 be Element of c1;
let c4, c5 be Subset of c1;
assume that E6: ( ( c2,c3 // c4 or c3,c2 // c4 ) & ( c2,c3 // c5 or c3,c2 // c5 ) )
and E7: c2 <> c3 ;
E8: ( c2,c3 // c4 & c2,c3 // c5 ) by E6, AFF_1:48;
hence c4 // c5 by E7, AFF_1:67;
thus c5 // c4 by E7, E8, AFF_1:67;
end;

theorem :: AFF_4:6
for b1 being AffinSpace
for b2, b3, b4, b5 being Element of b1
for b6 being Subset of b1 holds
( ( ) implies ( ( not b2,b3 // b6 & not b3,b2 // b6 ) or ( not b4,b5 // b6 & not b5,b4 // b6 ) or ( b2,b3 // b4,b5 & b2,b3 // b5,b4 ) ) )
proof
let c1 be AffinSpace;
let c2, c3, c4, c5 be Element of c1;
let c6 be Subset of c1;
assume E6: ( ( c2,c3 // c6 or c3,c2 // c6 ) & ( c4,c5 // c6 or c5,c4 // c6 ) ) ;
then E7: ( c2,c3 // c6 & c4,c5 // c6 ) by AFF_1:48;
c6 is is_line by E6, AFF_1:40;
hence c2,c3 // c4,c5 by E7, AFF_1:45;
hence c2,c3 // c5,c4 by AFF_1:13;
end;

theorem E6: :: AFF_4:7
for b1 being AffinSpace
for b2, b3, b4, b5 being Element of b1
for b6, b7 being Subset of b1 holds
( ( b2 in b6 & b3 in b6 & b4 in b7 ) implies ( ( not b6 // b7 & not b7 // b6 ) or not b2 <> b3 or ( not b2,b3 // b4,b5 & not b4,b5 // b2,b3 ) or b5 in b7 ) )
proof
let c1 be AffinSpace;
let c2, c3, c4, c5 be Element of c1;
let c6, c7 be Subset of c1;
assume E7: ( ( c6 // c7 or c7 // c6 ) & c2 <> c3 & ( c2,c3 // c4,c5 or c4,c5 // c2,c3 ) & c2 in c6 & c3 in c6 & c4 in c7 ) ;
then ( c6 is is_line & c7 is is_line ) by AFF_1:50;
then c2,c3 // c6 by E7, AFF_1:66;
then c4,c5 // c6 by E7, E5;
then c4,c5 // c7 by E7, E4;
hence c5 in c7 by E7, E3;
end;

E7: for b1 being AffinSpace
for b2, b3, b4 being Element of b1
for b5, b6 being Subset of b1 holds
not ( b5 // b6 & b2 in b5 & b3 in b5 & b4 in b6 & for b7 being Element of b1 holds
not ( b7 in b6 & b2,b4 // b3,b7 ) )
proof
let c1 be AffinSpace;
let c2, c3, c4 be Element of c1;
let c5, c6 be Subset of c1;
assume E8: ( c5 // c6 & c2 in c5 & c3 in c5 & c4 in c6 ) ;
then E9: c5 is is_line by AFF_1:50;
E10: now
assume E11: c2 <> c3 ;
consider c7 being Element of c1 such that
E12: c2,c3 // c4,c7
and E13: c2,c4 // c3,c7 by DIRAF:47;
c4,c7 // c2,c3 by E12, AFF_1:13;
then c4,c7 // c5 by E8, E9, E11, AFF_1:41;
then c4,c7 // c6 by E8, E4;
then c7 in c6 by E8, E3;
hence ex b1 being Element of c1 st
( b1 in c6 & c2,c4 // c3,b1 ) by E13;
end;
now
assume E11: c2 = c3 ;
take c7 = c4;
thus c7 in c6 by E8;
thus c2,c4 // c3,c7 by E11, AFF_1:11;
end;
hence ex b1 being Element of c1 st
( b1 in c6 & c2,c4 // c3,b1 ) by E10;
end;

theorem E8: :: AFF_4:8
for b1 being AffinSpace
for b2, b3, b4, b5, b6 being Element of b1
for b7, b8 being Subset of b1 holds
( ( b2 in b7 & b2 in b8 & b3 in b7 & b4 in b7 & b5 in b8 & b6 in b8 & b7 is is_line & b8 is is_line & b2 = b4 ) implies ( not b2 <> b3 or not b2 <> b5 or not b7 <> b8 or ( not b3,b5 // b4,b6 & not b5,b3 // b6,b4 ) or b2 = b6 ) )
proof
let c1 be AffinSpace;
let c2, c3, c4, c5, c6 be Element of c1;
let c7, c8 be Subset of c1;
assume that E9: ( c2 in c7 & c2 in c8 & c3 in c7 & c4 in c7 & c5 in c8 & c6 in c8 )
and E10: ( c2 <> c3 & c2 <> c5 & c7 <> c8 )
and E11: ( c3,c5 // c4,c6 or c5,c3 // c6,c4 )
and E12: ( c7 is is_line & c8 is is_line )
and E13: c2 = c4 ;
E14: ( LIN c2,c3,c4 & LIN c2,c5,c6 ) by E9, E12, AFF_1:33;
E15: not LIN c2,c3,c5
proof
assume LIN c2,c3,c5 ;
then consider c9 being Subset of c1 such that
E16: ( c9 is is_line & c2 in c9 & c3 in c9 & c5 in c9 ) by AFF_1:33;
( c7 = c9 & c8 = c9 ) by E9, E10, E12, E16, AFF_1:30;
hence not verum by E10;
end;
c3,c5 // c4,c6 by E11, AFF_1:13;
hence c2 = c6 by E13, E14, E15, AFF_1:69;
end;

theorem E9: :: AFF_4:9
for b1 being AffinSpace
for b2, b3, b4, b5, b6 being Element of b1
for b7, b8 being Subset of b1 holds
( ( b2 in b7 & b2 in b8 & b3 in b7 & b4 in b7 & b5 in b8 & b6 in b8 & b7 is is_line & b8 is is_line & b3 = b4 ) implies ( not b2 <> b3 or not b2 <> b5 or not b7 <> b8 or ( not b3,b5 // b4,b6 & not b5,b3 // b6,b4 ) or b5 = b6 ) )
proof
let c1 be AffinSpace;
let c2, c3, c4, c5, c6 be Element of c1;
let c7, c8 be Subset of c1;
assume that E10: ( c2 in c7 & c2 in c8 & c3 in c7 & c4 in c7 & c5 in c8 & c6 in c8 )
and E11: ( c2 <> c3 & c2 <> c5 & c7 <> c8 )
and E12: ( c3,c5 // c4,c6 or c5,c3 // c6,c4 )
and E13: ( c7 is is_line & c8 is is_line )
and E14: c3 = c4 ;
E15: ( LIN c2,c3,c4 & LIN c2,c5,c6 ) by E10, E13, AFF_1:33;
E16: not LIN c2,c3,c5
proof
assume LIN c2,c3,c5 ;
then consider c9 being Subset of c1 such that
E17: ( c9 is is_line & c2 in c9 & c3 in c9 & c5 in c9 ) by AFF_1:33;
( c7 = c9 & c8 = c9 ) by E10, E11, E13, E17, AFF_1:30;
hence not verum by E11;
end;
E17: ( LIN c2,c5,c5 & c3,c5 // c4,c5 ) by E14, AFF_1:11, AFF_1:16;
c3,c5 // c4,c6 by E12, AFF_1:13;
hence c5 = c6 by E15, E16, E17, AFF_1:70;
end;

theorem E10: :: AFF_4:10
for b1 being AffinSpace
for b2, b3, b4, b5 being Element of b1
for b6, b7 being Subset of b1 holds
( ( b2 in b6 & b3 in b6 & b4 in b7 & b5 in b7 & b2 = b3 ) implies ( ( not b6 // b7 & not b7 // b6 ) or not b6 <> b7 or ( not b2,b4 // b3,b5 & not b4,b2 // b5,b3 ) or b4 = b5 ) )
proof
let c1 be AffinSpace;
let c2, c3, c4, c5 be Element of c1;
let c6, c7 be Subset of c1;
assume that E11: ( c6 // c7 or c7 // c6 )
and E12: ( c2 in c6 & c3 in c6 & c4 in c7 & c5 in c7 )
and E13: c6 <> c7
and E14: ( c2,c4 // c3,c5 or c4,c2 // c5,c3 )
and E15: c2 = c3 ;
c2,c4 // c2,c5 by E14, E15, AFF_1:13;
then LIN c2,c4,c5 by AFF_1:def 1;
then E16: LIN c4,c5,c2 by AFF_1:15;
assume E17: c4 <> c5 ;
c7 is is_line by E11, AFF_1:50;
then c2 in c7 by E12, E16, E17, AFF_1:39;
hence not verum by E11, E12, E13, AFF_1:59;
end;

theorem E11: :: AFF_4:11
for b1 being AffinSpace
for b2, b3 being Element of b1 holds
ex b4 being Subset of b1 st
( b2 in b4 & b3 in b4 & b4 is is_line )
proof
let c1 be AffinSpace;
let c2, c3 be Element of c1;
LIN c2,c3,c3 by AFF_1:16;
then ex b1 being Subset of c1 st
( b1 is is_line & c2 in b1 & c3 in b1 & c3 in b1 ) by AFF_1:33;
hence ex b1 being Subset of c1 st
( c2 in b1 & c3 in b1 & b1 is is_line ) ;
end;

theorem E12: :: AFF_4:12
for b1 being AffinSpace
for b2 being Subset of b1 holds
not ( b2 is is_line & for b3 being Element of b1 holds b3 in b2 )
proof
let c1 be AffinSpace;
let c2 be Subset of c1;
assume E13: c2 is is_line ;
then consider c3, c4 being Element of c1 such that
E14: ( c3 in c2 & c4 in c2 & c3 <> c4 ) by AFF_1:31;
consider c5 being Element of c1 such that
E15: not LIN c3,c4,c5 by E14, AFF_1:22;
not c5 in c2 by E13, E14, E15, AFF_1:33;
hence not for b1 being Element of c1 holds b1 in c2 ;
end;

definition
let c1 be AffinSpace;
let c2, c3 be Subset of c1;
func Plane a2,a3 -> Subset of a1 equals :: AFF_4:def 1
{ b1 where B is Element of a1 : ex b1 being Element of a1 st
( b1,b2 // a2 & b2 in a3 ) } ;
coherence
{ b1 where B is Element of c1 : ex b1 being Element of c1 st
( b1,b2 // c2 & b2 in c3 ) } is Subset of c1
proof
set c4 = { b1 where B is Element of c1 : ex b1 being Element of c1 st
( b1,b2 // c2 & b2 in c3 ) } ;
now
let c5 be set ;
assume c5 in { b1 where B is Element of c1 : ex b1 being Element of c1 st
( b1,b2 // c2 & b2 in c3 ) } ;
then ex b1 being Element of c1 st
( b1 = c5 & ex b2 being Element of c1 st
( b1,b2 // c2 & b2 in c3 ) ) ;
hence c5 in the carrier of c1 ;
end;
hence { b1 where B is Element of c1 : ex b1 being Element of c1 st
( b1,b2 // c2 & b2 in c3 ) } is Subset of c1 by TARSKI:def 3;
end;
end;

:: deftheorem defines Plane AFF_4:def 1 :
for b1 being AffinSpace
for b2, b3 being Subset of b1 holds Plane b2,b3 = { b4 where B is Element of b1 : ex b1 being Element of b1 st
( b4,b5 // b2 & b5 in b3 ) } ;

definition
let c1 be AffinSpace;
let c2 be Subset of c1;
attr a2 is being_plane means :E13: :: AFF_4:def 2
ex b1, b2 being Subset of a1 st
( b1 is is_line & b2 is is_line & not b1 // b2 & a2 = Plane b1,b2 );
end;

:: deftheorem E13 defines being_plane AFF_4:def 2 :
for b1 being AffinSpace
for b2 being Subset of b1 holds
( b2 is being_plane iff ex b3, b4 being Subset of b1 st
( b3 is is_line & b4 is is_line & not b3 // b4 & b2 = Plane b3,b4 ) );

notation
let c1 be AffinSpace;
let c2 be Subset of c1;
end;

E14: for b1 being AffinSpace
for b2, b3 being Subset of b1
for b4 being Element of b1 holds
( b4 in Plane b2,b3 iff ex b5 being Element of b1 st
( b4,b5 // b2 & b5 in b3 ) )
proof
let c1 be AffinSpace;
let c2, c3 be Subset of c1;
let c4 be Element of c1;
E15: now
assume c4 in Plane c2,c3 ;
then c4 in { b1 where B is Element of c1 : ex b1 being Element of c1 st
( b1,b2 // c2 & b2 in c3 ) } ;
then ex b1 being Element of c1 st
( b1 = c4 & ex b2 being Element of c1 st
( b1,b2 // c2 & b2 in c3 ) ) ;
hence ex b1 being Element of c1 st
( c4,b1 // c2 & b1 in c3 ) ;
end;
now
assume ex b1 being Element of c1 st
( c4,b1 // c2 & b1 in c3 ) ;
then c4 in { b1 where B is Element of c1 : ex b1 being Element of c1 st
( b1,b2 // c2 & b2 in c3 ) } ;
hence c4 in Plane c2,c3 ;
end;
hence ( c4 in Plane c2,c3 iff ex b1 being Element of c1 st
( c4,b1 // c2 & b1 in c3 ) ) by E15;
end;

theorem :: AFF_4:13
for b1 being AffinSpace
for b2, b3 being Subset of b1 holds
( not b2 is is_line implies Plane b2,b3 = {} )
proof
let c1 be AffinSpace;
let c2, c3 be Subset of c1;
assume E15: not c2 is is_line ;
assume E16: Plane c2,c3 <> {} ;
consider c4 being Element of Plane c2,c3;
c4 in Plane c2,c3 by E16;
then c4 in { b1 where B is Element of c1 : ex b1 being Element of c1 st
( b1,b2 // c2 & b2 in c3 ) } ;
then ex b1 being Element of c1 st
( c4 = b1 & ex b2 being Element of c1 st
( b1,b2 // c2 & b2 in c3 ) ) ;
hence not verum by E15, AFF_1:40;
end;

theorem E15: :: AFF_4:14
for b1 being AffinSpace
for b2, b3 being Subset of b1 holds
( b2 is is_line implies b3 c= Plane b2,b3 )
proof
let c1 be AffinSpace;
let c2, c3 be Subset of c1;
assume E16: c2 is is_line ;
now
let c4 be set ;
assume E17: c4 in c3 ;
then reconsider c5 = c4 as Element of c1 ;
( c5,c5 // c2 & c5 in c3 ) by E16, E17, AFF_1:47;
then c4 in { b1 where B is Element of c1 : ex b1 being Element of c1 st
( b1,b2 // c2 & b2 in c3 ) } ;
hence c4 in Plane c2,c3 ;
end;
hence c3 c= Plane c2,c3 by TARSKI:def 3;
end;

theorem :: AFF_4:15
for b1 being AffinSpace
for b2, b3 being Subset of b1 holds
( b2 // b3 implies Plane b2,b3 = b3 )
proof
let c1 be AffinSpace;
let c2, c3 be Subset of c1;
assume E16: c2 // c3 ;
then E17: ( c2 is is_line & c3 is is_line ) by AFF_1:50;
set c4 = Plane c2,c3;
E18: c3 c= Plane c2,c3 by E17, E15;
Plane c2,c3 c= c3
proof
now
let c5 be set ;
assume c5 in Plane c2,c3 ;
then c5 in { b1 where B is Element of c1 : ex b1 being Element of c1 st
( b1,b2 // c2 & b2 in c3 ) } ;
then consider c6 being Element of c1 such that
E19: c5 = c6
and E20: ex b1 being Element of c1 st
( c6,b1 // c2 & b1 in c3 ) ;
consider c7 being Element of c1 such that
E21: c6,c7 // c2
and E22: c7 in c3 by E20;
c6,c7 // c3 by E16, E21, AFF_1:57;
then c7,c6 // c3 by AFF_1:48;
hence c5 in c3 by E17, E19, E22, AFF_1:37;
end;
hence Plane c2,c3 c= c3 by TARSKI:def 3;
end;
hence Plane c2,c3 = c3 by E18, XBOOLE_0:def 10;
end;

theorem E16: :: AFF_4:16
for b1 being AffinSpace
for b2, b3, b4 being Subset of b1 holds
( b2 // b3 implies Plane b2,b4 = Plane b3,b4 )
proof
let c1 be AffinSpace;
let c2, c3, c4 be Subset of c1;
assume E17: c2 // c3 ;
now
let c5 be set ;
thus ( c5 in Plane c2,c4 iff c5 in Plane c3,c4 )
proof
E18: now
assume c5 in Plane c2,c4 ;
then c5 in { b1 where B is Element of c1 : ex b1 being Element of c1 st
( b1,b2 // c2 & b2 in c4 ) } ;
then consider c6 being Element of c1 such that
E19: c5 = c6
and E20: ex b1 being Element of c1 st
( c6,b1 // c2 & b1 in c4 ) ;
consider c7 being Element of c1 such that
E21: ( c6,c7 // c2 & c7 in c4 ) by E20;
c6,c7 // c3 by E17, E21, AFF_1:57;
then c5 in { b1 where B is Element of c1 : ex b1 being Element of c1 st
( b1,b2 // c3 & b2 in c4 ) } by E19, E21;
hence c5 in Plane c3,c4 ;
end;
now
assume c5 in Plane c3,c4 ;
then c5 in { b1 where B is Element of c1 : ex b1 being Element of c1 st
( b1,b2 // c3 & b2 in c4 ) } ;
then consider c6 being Element of c1 such that
E19: c5 = c6
and E20: ex b1 being Element of c1 st
( c6,b1 // c3 & b1 in c4 ) ;
consider c7 being Element of c1 such that
E21: ( c6,c7 // c3 & c7 in c4 ) by E20;
c6,c7 // c2 by E17, E21, AFF_1:57;
then c5 in { b1 where B is Element of c1 : ex b1 being Element of c1 st
( b1,b2 // c2 & b2 in c4 ) } by E19, E21;
hence c5 in Plane c2,c4 ;
end;
hence ( c5 in Plane c2,c4 iff c5 in Plane c3,c4 ) by E18;
end;
end;
hence Plane c2,c4 = Plane c3,c4 by TARSKI:2;
end;

theorem :: AFF_4:17
for b1 being AffinSpace
for b2, b3, b4, b5, b6 being Element of b1
for b7, b8, b9, b10 being Subset of b1 holds
not ( b2 in b7 & b3 in b7 & b4 in b7 & b2 in b8 & b5 in b8 & b6 in b8 & not b2 in b9 & not b2 in b10 & b7 <> b8 & b3 in b9 & b5 in b9 & b4 in b10 & b6 in b10 & b7 is is_line & b8 is is_line & b9 is is_line & b10 is is_line & not b9 // b10 & for b11 being Element of b1 holds
not ( b11 in b9 & b11 in b10 ) )
proof
let c1 be AffinSpace;
let c2, c3, c4, c5, c6 be Element of c1;
let c7, c8, c9, c10 be Subset of c1;
assume that E17: ( c2 in c7 & c3 in c7 & c4 in c7 & c2 in c8 & c5 in c8 & c6 in c8 )
and E18: ( not c2 in c9 & not c2 in c10 & c7 <> c8 )
and E19: ( c3 in c9 & c5 in c9 & c4 in c10 & c6 in c10 )
and E20: ( c7 is is_line & c8 is is_line & c9 is is_line & c10 is is_line ) ;
E21: c3 <> c5 by E17, E18, E19, E20, AFF_1:30;
E22: c4 <> c6 by E17, E18, E19, E20, AFF_1:30;
LIN c2,c3,c4 by E17, E20, AFF_1:33;
then consider c11 being Element of c1 such that
E23: LIN c2,c5,c11
and E24: c3,c5 // c4,c11 by E18, E19, E2;
E25: c11 in c8 by E17, E18, E19, E20, E23, AFF_1:39;
then E26: c4 <> c11 by E17, E18, E19, E20, AFF_1:30;
set c12 = Line c4,c11;
E27: Line c4,c11 is is_line by E26, AFF_1:def 3;
E28: ( c4 in Line c4,c11 & c11 in Line c4,c11 ) by AFF_1:26;
now
assume Line c4,c11 <> c10 ;
then E29: c11 <> c6 by E19, E20, E22, E27, E28, AFF_1:30;
LIN c6,c11,c5 by E17, E20, E25, AFF_1:33;
then consider c13 being Element of c1 such that
E30: LIN c6,c4,c13
and E31: c11,c4 // c5,c13 by E29, E2;
E32: c13 in c10 by E19, E20, E22, E30, AFF_1:39;
c5,c3 // c11,c4 by E24, AFF_1:13;
then c5,c3 // c5,c13 by E26, E31, AFF_1:14;
then LIN c5,c3,c13 by AFF_1:def 1;
then c13 in c9 by E19, E20, E21, AFF_1:39;
hence ex b1 being Element of c1 st
( b1 in c9 & b1 in c10 ) by E32;
end;
hence not ( not c9 // c10 & for b1 being Element of c1 holds
not ( b1 in c9 & b1 in c10 ) ) by E19, E20, E21, E24, E26, E28, AFF_1:52;
end;

theorem E17: :: AFF_4:18
for b1 being AffinSpace
for b2, b3, b4, b5 being Element of b1
for b6, b7, b8, b9 being Subset of b1 holds
not ( b2 in b6 & b3 in b6 & b4 in b7 & b5 in b7 & b2 in b8 & b4 in b8 & b3 in b9 & b5 in b9 & b6 <> b7 & b6 // b7 & b8 is is_line & b9 is is_line & not b8 // b9 & for b10 being Element of b1 holds
not ( b10 in b8 & b10 in b9 ) )
proof
let c1 be AffinSpace;
let c2, c3, c4, c5 be Element of c1;
let c6, c7, c8, c9 be Subset of c1;
assume that E18: ( c2 in c6 & c3 in c6 & c4 in c7 & c5 in c7 & c2 in c8 & c4 in c8 & c3 in c9 & c5 in c9 )
and E19: c6 <> c7
and E20: c6 // c7
and E21: ( c8 is is_line & c9 is is_line ) ;
E22: ( c6 is is_line & c7 is is_line ) by E20, AFF_1:50;
E23: ( c2 <> c4 & c3 <> c5 ) by E18, E19, E20, AFF_1:59;
now
assume E24: c2 <> c3 ;
consider c10 being Element of c1 such that
E25: c2,c3 // c4,c10
and E26: c2,c4 // c3,c10 by DIRAF:47;
c2,c3 // c6 by E18, E22, AFF_1:66;
then c2,c3 // c7 by E20, AFF_1:57;
then c4,c10 // c7 by E24, E25, AFF_1:46;
then E27: c10 in c7 by E18, E22, AFF_1:37;
then E28: c3 <> c10 by E18, E19, E20, AFF_1:59;
set c11 = Line c3,c10;
E29: Line c3,c10 is is_line by E28, AFF_1:def 3;
E30: ( c3 in Line c3,c10 & c10 in Line c3,c10 ) by AFF_1:26;
now
assume Line c3,c10 <> c9 ;
then E31: c10 <> c5 by E18, E21, E23, E29, E30, AFF_1:30;
LIN c5,c10,c4 by E18, E22, E27, AFF_1:33;
then consider c12 being Element of c1 such that
E32: LIN c5,c3,c12
and E33: c10,c3 // c4,c12 by E31, E2;
E34: c12 in c9 by E18, E21, E23, E32, AFF_1:39;
c4,c2 // c10,c3 by E26, AFF_1:13;
then c4,c2 // c4,c12 by E28, E33, AFF_1:14;
then LIN c4,c2,c12 by AFF_1:def 1;
then c12 in c8 by E18, E21, E23, AFF_1:39;
hence ex b1 being Element of c1 st
( b1 in c8 & b1 in c9 ) by E34;
end;
hence not ( not c8 // c9 & for b1 being Element of c1 holds
not ( b1 in c8 & b1 in c9 ) ) by E18, E21, E23, E26, E28, E30, AFF_1:52;
end;
hence not ( not c8 // c9 & for b1 being Element of c1 holds
not ( b1 in c8 & b1 in c9 ) ) by E18;
end;

E18: for b1 being AffinSpace
for b2 being Element of b1
for b3, b4, b5 being Subset of b1 holds
( ( b3 is is_line & b4 is is_line & b2 in b5 & b2 in Plane b3,b4 & b3 // b5 ) implies ( b5 c= Plane b3,b4 ) )
proof
let c1 be AffinSpace;
let c2 be Element of c1;
let c3, c4, c5 be Subset of c1;
assume E19: ( c3 is is_line & c4 is is_line & c2 in c5 & c2 in Plane c3,c4 & c3 // c5 ) ;
now
let c6 be set ;
assume E20: c6 in c5 ;
consider c7 being Element of c1 such that
E21: ( c2,c7 // c3 & c7 in c4 ) by E19, E14;
E22: Plane c3,c4 = Plane c5,c4 by E19, E16;
E23: c5 is is_line by E19, AFF_1:50;
c2,c7 // c5 by E19, E21, AFF_1:57;
then E24: c7 in c5 by E19, E23, AFF_1:37;
reconsider c8 = c6 as Element of c1 by E20;
c8,c7 // c5 by E20, E23, E24, AFF_1:37;
hence c6 in Plane c3,c4 by E21, E22;
end;
hence c5 c= Plane c3,c4 by TARSKI:def 3;
end;

E19: for b1 being AffinSpace
for b2, b3 being Element of b1
for b4, b5, b6 being Subset of b1 holds
( ( b4 is is_line & b5 is is_line & b6 is is_line & b2 in Plane b4,b5 & b3 in Plane b4,b5 & b2 in b6 & b3 in b6 ) implies ( not b2 <> b3 or b6 c= Plane b4,b5 ) )
proof
let c1 be AffinSpace;
let c2, c3 be Element of c1;
let c4, c5, c6 be Subset of c1;
assume E20: ( c4 is is_line & c5 is is_line & c6 is is_line & c2 in Plane c4,c5 & c3 in Plane c4,c5 & c2 <> c3 & c2 in c6 & c3 in c6 ) ;
now
let c7 be set ;
assume E21: c7 in c6 ;
then reconsider c8 = c7 as Element of the carrier of c1 ;
consider c9 being Element of c1 such that
E22: ( c2,c9 // c4 & c9 in c5 ) by E20, E14;
consider c10 being Element of c1 such that
E23: ( c3,c10 // c4 & c10 in c5 ) by E20, E14;
consider c11 being Subset of c1 such that
E24: ( c2 in c11 & c4 // c11 ) by E20, AFF_1:63;
consider c12 being Subset of c1 such that
E25: ( c3 in c12 & c4 // c12 ) by E20, AFF_1:63;
E26: c11 // c12 by E24, E25, AFF_1:58;
E27: ( c2,c9 // c11 & c3,c10 // c12 ) by E22, E23, E24, E25, AFF_1:57;
then E28: ( c9 in c11 & c10 in c12 ) by E24, E25, E3;
E29: ( c11 is is_line & c12 is is_line ) by E27, AFF_1:40;
E30: now
assume c11 = c12 ;
then c6 = c11 by E20, E24, E25, E29, AFF_1:30;
then c6 c= Plane c4,c5 by E20, E24, E18;
hence c7 in Plane c4,c5 by E21;
end;
now
assume c11 <> c12 ;
then E31: not ( not c5 // c6 & for b1 being Element of c1 holds
not ( b1 in c5 & b1 in c6 ) ) by E20, E22, E23, E24, E25, E26, E28, E17;
E32: now
assume E33: c5 // c6 ;
E34: now
assume E35: c5 = c6 ;
c8,c8 // c4 by E20, AFF_1:47;
hence c7 in Plane c4,c5 by E21, E35;
end;
now
assume c5 <> c6 ;
then E35: c3 <> c10 by E20, E23, E33, AFF_1:59;
now
assume E36: c8 <> c3 ;
consider c13 being Element of c1 such that
E37: ( c3,c8 // c10,c13 & c3,c10 // c8,c13 ) by DIRAF:47;
c3,c8 // c6 by E20, E21, AFF_1:37;
then c10,c13 // c6 by E36, E37, AFF_1:46;
then c10,c13 // c5 by E33, AFF_1:57;
then E38: c13 in c5 by E23, E3;
c8,c13 // c4 by E23, E35, E37, AFF_1:46;
hence c7 in Plane c4,c5 by E38;
end;
hence c7 in Plane c4,c5 by E20;
end;
hence c7 in Plane c4,c5 by E34;
end;
now
given c13 being Element of c1 such that E33: ( c13 in c5 & c13 in c6 )
and E34: not c5 // c6 ;
E35: c5 <> c6 by E20, E34, AFF_1:55;
E36: now
assume E37: c13 <> c2 ;
then E38: c2 <> c9 by E20, E22, E33, E35, AFF_1:30;
E39: now
assume E40: c13 = c9 ;
c2,c13 // c6 by E20, E33, AFF_1:37;
then c4 // c6 by E22, E37, E40, AFF_1:67;
then c6 c= Plane c4,c5 by E20, E18;
hence c7 in Plane c4,c5 by E21;
end;
now
assume E40: c13 <> c9 ;
LIN c13,c2,c8 by E20, E21, E33, AFF_1:33;
then consider c14 being Element of c1 such that
E41: ( LIN c13,c9,c14 & c2,c9 // c8,c14 ) by E37, E2;
E42: c13,c9 // c13,c14 by E41, AFF_1:def 1;
c13,c9 // c5 by E20, E22, E33, AFF_1:37;
then c13,c14 // c5 by E40, E42, AFF_1:46;
then E43: c14 in c5 by E33, E3;
c8,c14 // c4 by E22, E38, E41, AFF_1:46;
hence c7 in Plane c4,c5 by E43;
end;
hence c7 in Plane c4,c5 by E39;
end;
now
assume E37: c13 <> c3 ;
then E38: c3 <> c10 by E20, E23, E33, E35, AFF_1:30;
E39: now
assume E40: c13 = c10 ;
c3,c13 // c6 by E20, E33, AFF_1:37;
then c4 // c6 by E23, E37, E40, AFF_1:67;
then c6 c= Plane c4,c5 by E20, E18;
hence c7 in Plane c4,c5 by E21;
end;
now
assume E40: c13 <> c10 ;
LIN c13,c3,c8 by E20, E21, E33, AFF_1:33;
then consider c14 being Element of c1 such that
E41: ( LIN c13,c10,c14 & c3,c10 // c8,c14 ) by E37, E2;
E42: c13,c10 // c13,c14 by E41, AFF_1:def 1;
c13,c10 // c5 by E20, E23, E33, AFF_1:37;
then c13,c14 // c5 by E40, E42, AFF_1:46;
then E43: c14 in c5 by E33, E3;
c8,c14 // c4 by E23, E38, E41, AFF_1:46;
hence c7 in Plane c4,c5 by E43;
end;
hence c7 in Plane c4,c5 by E39;
end;
hence c7 in Plane c4,c5 by E20, E36;
end;
hence c7 in Plane c4,c5 by E31, E32;
end;
hence c7 in Plane c4,c5 by E30;
end;
hence c6 c= Plane c4,c5 by TARSKI:def 3;
end;

theorem E20: :: AFF_4:19
for b1 being AffinSpace
for b2, b3 being Element of b1
for b4 being Subset of b1 holds
( ( b4 is is_plane & b2 in b4 & b3 in b4 ) implies ( not b2 <> b3 or Line b2,b3 c= b4 ) )
proof
let c1 be AffinSpace;
let c2, c3 be Element of c1;
let c4 be Subset of c1;
assume that E21: c4 is is_plane
and E22: ( c2 in c4 & c3 in c4 )
and E23: c2 <> c3 ;
set c5 = Line c2,c3;
E24: Line c2,c3 is is_line by E23, AFF_1:def 3;
E25: ( c2 in Line c2,c3 & c3 in Line c2,c3 ) by AFF_1:26;
ex b1, b2 being Subset of c1 st
( b1 is is_line & b2 is is_line & not b1 // b2 & c4 = Plane b1,b2 ) by E21, E13;
hence Line c2,c3 c= c4 by E22, E23, E24, E25, E19;
end;

E21: for b1 being AffinSpace
for b2, b3, b4 being Subset of b1 holds
( ( b2 is is_line & b3 is is_line & b4 is is_line & b4 c= Plane b2,b3 ) implies ( Plane b2,b4 c= Plane b2,b3 ) )
proof
let c1 be AffinSpace;
let c2, c3, c4 be Subset of c1;
assume that E22: ( c2 is is_line & c3 is is_line & c4 is is_line )
and E23: c4 c= Plane c2,c3 ;
now
let c5 be set ;
assume c5 in Plane c2,c4 ;
then c5 in { b1 where B is Element of c1 : ex b1 being Element of c1 st
( b1,b2 // c2 & b2 in c4 ) } ;
then consider c6 being Element of c1 such that
E24: c5 = c6
and E25: ex b1 being Element of c1 st
( c6,b1 // c2 & b1 in c4 ) ;
consider c7 being Element of c1 such that
E26: c6,c7 // c2
and E27: c7 in c4 by E25;
consider c8 being Element of c1 such that
E28: c7,c8 // c2
and E29: c8 in c3 by E23, E27, E14;
consider c9 being Subset of c1 such that
E30: c7 in c9
and E31: c2 // c9 by E22, AFF_1:63;
E32: c9 // c2 by E31;
( c6,c7 // c9 & c7,c8 // c9 ) by E26, E28, E31, AFF_1:57;
then ( c6 in c9 & c8 in c9 ) by E30, E3;
then c6,c8 // c2 by E32, AFF_1:54;
hence c5 in Plane c2,c3 by E24, E29;
end;
hence Plane c2,c4 c= Plane c2,c3 by TARSKI:def 3;
end;

theorem E22: :: AFF_4:20
for b1 being AffinSpace
for b2, b3, b4 being Subset of b1 holds
( ( b2 is is_line & b3 is is_line & b4 is is_line & b4 c= Plane b2,b3 ) implies ( b2 // b3 or b2 // b4 or Plane b2,b4 = Plane b2,b3 ) )
proof
let c1 be AffinSpace;
let c2, c3, c4 be Subset of c1;
assume that E23: ( c2 is is_line & c3 is is_line & c4 is is_line )
and E24: ( not c2 // c3 & not c2 // c4 )
and E25: c4 c= Plane c2,c3 ;
E26: Plane c2,c4 c= Plane c2,c3 by E23, E25, E21;
consider c5, c6 being Element of c1 such that
E27: ( c5 in c4 & c6 in c4 )
and E28: c5 <> c6 by E23, AFF_1:31;
consider c7 being Element of c1 such that
E29: c5,c7 // c2
and E30: c7 in c3 by E25, E27, E14;
consider c8 being Element of c1 such that
E31: c6,c8 // c2
and E32: c8 in c3 by E25, E27, E14;
E33: c7 <> c8
proof
assume E34: c7 = c8 ;
consider c9 being Subset of c1 such that
E35: c7 in c9
and E36: c2 // c9 by E23, AFF_1:63;
E37: c9 is is_line by E36, AFF_1:50;
( c7,c6 // c9 & c7,c5 // c9 ) by E29, E31, E34, E36, E4;
then ( c6 in c9 & c5 in c9 ) by E35, E3;
hence not verum by E23, E24, E27, E28, E36, E37, AFF_1:30;
end;
( c7,c5 // c2 & c8,c6 // c2 ) by E29, E31, AFF_1:48;
then ( c7 in Plane c2,c4 & c8 in Plane c2,c4 ) by E27;
then c3 c= Plane c2,c4 by E23, E30, E32, E33, E19;
then Plane c2,c3 c= Plane c2,c4 by E23, E21;
hence Plane c2,c4 = Plane c2,c3 by E26, XBOOLE_0:def 10;
end;

theorem E23: :: AFF_4:21
for b1 being AffinSpace
for b2, b3, b4 being Subset of b1 holds
not ( b2 is is_line & b3 is is_line & b4 is is_line & b4 c= Plane b2,b3 & not b3 // b4 & for b5 being Element of b1 holds
not ( b5 in b3 & b5 in b4 ) )
proof
let c1 be AffinSpace;
let c2, c3, c4 be Subset of c1;
assume that E24: ( c2 is is_line & c3 is is_line & c4 is is_line )
and E25: c4 c= Plane c2,c3 ;
consider c5, c6 being Element of c1 such that
E26: ( c5 in c4 & c6 in c4 )
and E27: c5 <> c6 by E24, AFF_1:31;
consider c7 being Element of c1 such that
E28: c5,c7 // c2
and E29: c7 in c3 by E25, E26, E14;
consider c8 being Element of c1 such that
E30: c6,c8 // c2
and E31: c8 in c3 by E25, E26, E14;
consider c9 being Subset of c1 such that
E32: c7 in c9
and E33: c2 // c9 by E24, AFF_1:63;
consider c10 being Subset of c1 such that
E34: c8 in c10
and E35: c2 // c10 by E24, AFF_1:63;
E36: ( c7,c5 // c9 & c8,c6 // c10 & c9 // c10 ) by E28, E30, E33, E35, E4, AFF_1:58;
then E37: ( c5 in c9 & c6 in c10 ) by E32, E34, E3;
E38: ( c9 is is_line & c10 is is_line ) by E33, E35, AFF_1:50;
now
assume c9 = c10 ;
then ( c6 in c9 & c5 in c9 ) by E32, E34, E36, E3;
then c7 in c4 by E24, E26, E27, E32, E38, AFF_1:30;
hence ex b1 being Element of c1 st
( b1 in c3 & b1 in c4 ) by E29;
end;
hence not ( not c3 // c4 & for b1 being Element of c1 holds
not ( b1 in c3 & b1 in c4 ) ) by E24, E26, E29, E31, E32, E34, E36, E37, E17;
end;

theorem E24: :: AFF_4:22
for b1 being AffinSpace
for b2, b3, b4 being Subset of b1 holds
not ( b2 is is_plane & b3 is is_line & b4 is is_line & b3 c= b2 & b4 c= b2 & not b3 // b4 & for b5 being Element of b1 holds
not ( b5 in b3 & b5 in b4 ) )
proof
let c1 be AffinSpace;
let c2, c3, c4 be Subset of c1;
assume that E25: c2 is is_plane
and E26: ( c3 is is_line & c4 is is_line )
and E27: ( c3 c= c2 & c4 c= c2 ) ;
consider c5, c6 being Subset of c1 such that
E28: ( c5 is is_line & c6 is is_line )
and E29: not c5 // c6
and E30: c2 = Plane c5,c6 by E25, E13;
E31: now
assume not c5 // c3 ;
then c4 c= Plane c5,c3 by E26, E27, E28, E29, E30, E22;
hence not ( not c3 // c4 & for b1 being Element of c1 holds
not ( b1 in c3 & b1 in c4 ) ) by E26, E28, E23;
end;
now
assume not c5 // c4 ;
then c3 c= Plane c5,c4 by E26, E27, E28, E29, E30, E22;
then not ( not c4 // c3 & for b1 being Element of c1 holds
not ( b1 in c4 & b1 in c3 ) ) by E26, E28, E23;
hence not ( not c3 // c4 & for b1 being Element of c1 holds
not ( b1 in c3 & b1 in c4 ) ) ;
end;
hence not ( not c3 // c4 & for b1 being Element of c1 holds
not ( b1 in c3 & b1 in c4 ) ) by E31, AFF_1:58;
end;

theorem E25: :: AFF_4:23
for b1 being AffinSpace
for b2 being Element of b1
for b3, b4, b5 being Subset of b1 holds
( ( b3 is is_plane & b2 in b3 & b4 c= b3 & b2 in b5 ) implies ( ( not b4 // b5 & not b5 // b4 ) or b5 c= b3 ) )
proof
let c1 be AffinSpace;
let c2 be Element of c1;
let c3, c4, c5 be Subset of c1;
assume that E26: c3 is is_plane
and E27: ( c2 in c3 & c4 c= c3 )
and E28: c2 in c5
and E29: ( c4 // c5 or c5 // c4 ) ;
E30: ( c4 is is_line & c5 is is_line ) by E29, AFF_1:50;
consider c6, c7 being Subset of c1 such that
E31: ( c6 is is_line & c7 is is_line )
and E32: not c6 // c7
and E33: c3 = Plane c6,c7 by E26, E13;
E34: now
assume c6 // c4 ;
then c6 // c5 by E29, AFF_1:58;
hence c5 c=