let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for a, b being POINT of S
for E being Subset of S st E is_plane & a in E & b in E & a <> b holds
( Line (a,b) c= E & ex c being POINT of S st
( not Collinear a,b,c & E = Plane (a,b,c) ) )
let a, b be POINT of S; :: thesis: for E being Subset of S st E is_plane & a in E & b in E & a <> b holds
( Line (a,b) c= E & ex c being POINT of S st
( not Collinear a,b,c & E = Plane (a,b,c) ) )
let E be Subset of S; :: thesis: ( E is_plane & a in E & b in E & a <> b implies ( Line (a,b) c= E & ex c being POINT of S st
( not Collinear a,b,c & E = Plane (a,b,c) ) ) )
assume that
A1: E is_plane and
A2: a in E and
A3: b in E and
A4: a <> b ; :: thesis: ( Line (a,b) c= E & ex c being POINT of S st
( not Collinear a,b,c & E = Plane (a,b,c) ) )
consider p, q, r being POINT of S such that
A5: not Collinear p,q,r and
A6: E = Plane (p,q,r) by A1;
A7: p <> q by A5, GTARSKI3:46;
set A = Line (p,q);
set A9 = Line (a,b);

per cases ( Line (p,q) = Line (a,b) or Line (p,q) <> Line (a,b) ) ;

suppose A8: Line (p,q) = Line (a,b) ; :: thesis: ( Line (a,b) c= E & ex c being POINT of S st
( not Collinear a,b,c & E = Plane (a,b,c) ) )

then A9: E = Plane ((Line (a,b)),r) by A5, A6, Def11;
A10: not r in Line (a,b)

proof

assume r in Line (a,b) ; :: thesis: contradiction
then ex s being POINT of S st
( r = s & Collinear p,q,s ) by A8;
hence contradiction by A5; :: thesis: verum

end;

Line (a,b) is_line by A4;
hence Line (a,b) c= E by A9, A10, Th31; :: thesis: ex c being POINT of S st
( not Collinear a,b,c & E = Plane (a,b,c) )
R1: not Collinear a,b,r by A10;
then Plane (a,b,r) = Plane ((Line (a,b)),r) by Def11;
hence ex c being POINT of S st
( not Collinear a,b,c & E = Plane (a,b,c) ) by R1, A8, A5, A6, Def11; :: thesis: verum

end;

suppose A11: Line (p,q) <> Line (a,b) ; :: thesis: ( Line (a,b) c= E & ex c being POINT of S st
( not Collinear a,b,c & E = Plane (a,b,c) ) )

( not a in Line (p,q) or not b in Line (p,q) )

proof

assume A12: ( a in Line (p,q) & b in Line (p,q) ) ; :: thesis: contradiction
Line (p,q) is_line by A7;
hence contradiction by A11, A12, A4, GTARSKI3:87; :: thesis: verum

end;

per cases then ( not a in Line (p,q) or not b in Line (p,q) ) ;

suppose A13: not a in Line (p,q) ; :: thesis: ( Line (a,b) c= E & ex c being POINT of S st
( not Collinear a,b,c & E = Plane (a,b,c) ) )

then consider c being POINT of S such that
A14: not Collinear b,a,c and
A15: E = Plane (b,a,c) by A11, A2, A3, A4, A5, A6, Th45;
A16: not Collinear a,b,c by GTARSKI3:45, A14;
E = Plane ((Line (a,b)),c) by A15, A14, Def11
.= Plane (a,b,c) by A16, Def11 ;
hence ( Line (a,b) c= E & ex c being POINT of S st
( not Collinear a,b,c & E = Plane (a,b,c) ) ) by A16, A11, A13, A2, A3, A4, A5, A6, Th45; :: thesis: verum

end;

suppose not b in Line (p,q) ; :: thesis: ( Line (a,b) c= E & ex c being POINT of S st
( not Collinear a,b,c & E = Plane (a,b,c) ) )

hence ( Line (a,b) c= E & ex c being POINT of S st
( not Collinear a,b,c & E = Plane (a,b,c) ) ) by A11, A2, A3, A4, A5, A6, Th45; :: thesis: verum

end;

end;

end;

end;