:: AFF_4 semantic presentation

Lemma1: 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 Th1: :: 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 Th2: :: AFF_4:2
for b1 being AffinSpace
for b2, b3 being Element of b1
for b4 being Subset of b1 holds
( ( b2,b3 // b4 or b3,b2 // b4 ) & b2 in b4 implies 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_line ) by E4, AFF_1:40, AFF_1:48;
hence c3 in c4 by E5, AFF_1:37;
end;

theorem Th3: :: AFF_4:3
for b1 being AffinSpace
for b2, b3 being Element of b1
for b4, b5 being Subset of b1 holds
( ( b2,b3 // b4 or b3,b2 // b4 ) & b4 // b5 implies ( 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 ;
( 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 Th4: :: AFF_4:4
for b1 being AffinSpace
for b2, b3, b4, b5 being Element of b1
for b6 being Subset of b1 holds
( ( b2,b3 // b6 or b3,b2 // b6 ) & ( b2,b3 // b4,b5 or b4,b5 // b2,b3 ) & b2 <> b3 implies ( 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 Th5: :: AFF_4:5
for b1 being AffinSpace
for b2, b3 being Element of b1
for b4, b5 being Subset of b1 holds
( ( b2,b3 // b4 or b3,b2 // b4 ) & ( b2,b3 // b5 or b3,b2 // b5 ) & b2 <> b3 implies b4 // b5 )
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 ;
( c2,c3 // c4 & c2,c3 // c5 ) by E6, AFF_1:48;
hence c4 // c5 by E7, AFF_1:67;
end;

theorem Th6: :: AFF_4:6
for b1 being AffinSpace
for b2, b3, b4, b5 being Element of b1
for b6 being Subset of b1 holds
( ( b2,b3 // b6 or b3,b2 // b6 ) & ( b4,b5 // b6 or b5,b4 // b6 ) implies b2,b3 // b4,b5 )
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_line by E6, AFF_1:40;
hence c2,c3 // c4,c5 by E7, AFF_1:45;
end;

theorem Th7: :: AFF_4:7
for b1 being AffinSpace
for b2, b3, b4, b5 being Element of b1
for b6, b7 being Subset of b1 holds
( ( b6 // b7 or b7 // b6 ) & b2 <> b3 & ( b2,b3 // b4,b5 or b4,b5 // b2,b3 ) & b2 in b6 & b3 in b6 & b4 in b7 implies 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_line & c7 is_line ) by AFF_1:50;
then c2,c3 // c6 by E7, AFF_1:66;
then c4,c5 // c6 by E7, Th4;
then c4,c5 // c7 by E7, Th3;
hence c5 in c7 by E7, Th2;
end;

Lemma7: 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_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, Th3;
then c7 in c6 by E8, Th2;
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 Th8: :: 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 & b2 <> b3 & b2 <> b5 & b7 <> b8 & ( b3,b5 // b4,b6 or b5,b3 // b6,b4 ) & b7 is_line & b8 is_line & b2 = b4 implies 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_line & c8 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_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 Th9: :: 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 & b2 <> b3 & b2 <> b5 & b7 <> b8 & ( b3,b5 // b4,b6 or b5,b3 // b6,b4 ) & b7 is_line & b8 is_line & b3 = b4 implies 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_line & c8 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_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 Th10: :: AFF_4:10
for b1 being AffinSpace
for b2, b3, b4, b5 being Element of b1
for b6, b7 being Subset of b1 holds
( ( b6 // b7 or b7 // b6 ) & b2 in b6 & b3 in b6 & b4 in b7 & b5 in b7 & b6 <> b7 & ( b2,b4 // b3,b5 or b4,b2 // b5,b3 ) & b2 = b3 implies 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_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 Th11: :: 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_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_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_line ) ;
end;

theorem Th12: :: AFF_4:12
for b1 being AffinSpace
for b2 being Subset of b1 holds
not ( b2 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_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 c2,c3 -> 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 Def1 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 :Def2: :: AFF_4:def 2
ex b1, b2 being Subset of a1 st
( b1 is_line & b2 is_line & not b1 // b2 & a2 = Plane b1,b2 );
end;

:: deftheorem Def2 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_line & b4 is_line & not b3 // b4 & b2 = Plane b3,b4 ) );

notation
let c1 be AffinSpace;
let c2 be Subset of c1;
synonym c2 is_plane for being_plane c2;
end;

Lemma14: 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;
thus ( c4 in Plane c2,c3 iff ex b1 being Element of c1 st
( c4,b1 // c2 & b1 in c3 ) ) by E15;
end;

theorem Th13: :: AFF_4:13
for b1 being AffinSpace
for b2, b3 being Subset of b1 holds
( not b2 is_line implies Plane b2,b3 = {} )
proof
let c1 be AffinSpace;
let c2, c3 be Subset of c1;
assume E15: not c2 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 Th14: :: AFF_4:14
for b1 being AffinSpace
for b2, b3 being Subset of b1 holds
( b2 is_line implies b3 c= Plane b2,b3 )
proof
let c1 be AffinSpace;
let c2, c3 be Subset of c1;
assume E16: c2 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 Th15: :: 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_line & c3 is_line ) by AFF_1:50;
set c4 = Plane c2,c3;
E18: c3 c= Plane c2,c3 by E17, Th14;
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 Th16: :: 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 Th17: :: 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_line & b8 is_line & b9 is_line & b10 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_line & c8 is_line & c9 is_line & c10 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, Th1;
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_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, Th1;
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 Th18: :: 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_line & b9 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_line & c9 is_line ) ;
E22: ( c6 is_line & c7 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_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, Th1;
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;

Lemma18: for b1 being AffinSpace
for b2 being Element of b1
for b3, b4, b5 being Subset of b1 holds
( b3 is_line & b4 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_line & c4 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, Lemma14;
E22: Plane c3,c4 = Plane c5,c4 by E19, Th16;
E23: c5 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;

Lemma19: for b1 being AffinSpace
for b2, b3 being Element of b1
for b4, b5, b6 being Subset of b1 holds
( b4 is_line & b5 is_line & b6 is_line & b2 in Plane b4,b5 & b3 in Plane b4,b5 & b2 <> b3 & b2 in b6 & b3 in b6 implies 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_line & c5 is_line & c6 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, Lemma14;
consider c10 being Element of c1 such that
E23: ( c3,c10 // c4 & c10 in c5 ) by E20, Lemma14;
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, Th2;
E29: ( c11 is_line & c12 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, Lemma18;
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, Th18;
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, Th2;
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, Lemma18;
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, Th1;
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, Th2;
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, Lemma18;
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, Th1;
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, Th2;
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 Th19: :: AFF_4:19
for b1 being AffinSpace
for b2, b3 being Element of b1
for b4 being Subset of b1 holds
( b4 is_plane & b2 in b4 & b3 in b4 & b2 <> b3 implies 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_plane and
E22: ( c2 in c4 & c3 in c4 ) and
E23: c2 <> c3 ;
set c5 = Line c2,c3;
E24: Line c2,c3 is_line by E23, AFF_1:def 3;
E25: ( c2 in Line c2,c3 & c3 <