let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for a, b, c, p, q, r being POINT of S
for E being Subset of S st a in E & b in E & a <> b & not Collinear p,q,r & E = Plane (p,q,r) & c in Line (p,q) & not c in Line (a,b) & not b in Line (p,q) 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, c, p, q, r be POINT of S; :: thesis: for E being Subset of S st a in E & b in E & a <> b & not Collinear p,q,r & E = Plane (p,q,r) & c in Line (p,q) & not c in Line (a,b) & not b in Line (p,q) 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: ( a in E & b in E & a <> b & not Collinear p,q,r & E = Plane (p,q,r) & c in Line (p,q) & not c in Line (a,b) & not b in Line (p,q) 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: a in E and
A2: b in E and
A3: a <> b and
A4: not Collinear p,q,r and
A5: E = Plane (p,q,r) and
A6: c in Line (p,q) and
A7: not c in Line (a,b) and
A8: 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) ) )
set A = Line (p,q);
set A9 = Line (a,b);
set A99 = Line (c,b);
A9: not r in Line (p,q)

proof

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

end;

per cases ( c = b or c <> b ) ;

suppose c = 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 Collinear a,b,c by GTARSKI4:4;
hence ( Line (a,b) c= E & ex c being POINT of S st
( not Collinear a,b,c & E = Plane (a,b,c) ) ) by A7; :: thesis: verum

end;

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

A11: p <> q by A4, GTARSKI3:46;
then A12: ( Line (p,q) is_line & Line (a,b) is_line & Line (c,b) is_line ) by A10, A3;
A13: Line (p,q) <> Line (c,b) by A8, GTARSKI3:83;
A14: Line (p,q), Line (c,b) Is c by A6, A8, A12, GTARSKI3:83;
A15: ( not r in Line (p,q) & not b in Line (p,q) & b in Plane ((Line (p,q)),r) ) by A9, A8, A2, A4, A5, Def11;
T1: ( Line (p,q) is_line & Line (c,b) is_line ) by A11, A10;
( c in Line (p,q) & c in Line (c,b) ) by A6, GTARSKI3:83;
then not (Line (p,q)) /\ (Line (c,b)) is empty by XBOOLE_0:def 4;
then consider r99 being POINT of S such that
A16: not r99 in Line (p,q) and
r99 in Line (c,b) and
A17: Plane ((Line (p,q)),(Line (c,b))) = Plane ((Line (p,q)),r99) by T1, A13, Def13;
e2: ( Line (c,b) c= Plane ((Line (p,q)),(Line (c,b))) & b in Line (c,b) ) by A14, Th43, GTARSKI3:83;
A19: E = Plane ((Line (p,q)),r) by A4, A5, Def11
.= Plane ((Line (p,q)),b) by A12, A15, Th34
.= Plane ((Line (p,q)),(Line (c,b))) by A8, A16, e2, A17, A12, Th34 ;
W1: ( Line (p,q) is_line & Line (c,b) is_line ) by A11, A10;
( c in Line (p,q) & c in Line (c,b) ) by A6, GTARSKI3:83;
then not (Line (c,b)) /\ (Line (p,q)) is empty by XBOOLE_0:def 4;
then consider r999 being POINT of S such that
A20: not r999 in Line (c,b) and
r999 in Line (p,q) and
A21: Plane ((Line (c,b)),(Line (p,q))) = Plane ((Line (c,b)),r999) by W1, A13, Def13;
A22: not a in Line (c,b)

proof

assume A23: a in Line (c,b) ; :: thesis: contradiction
b in Line (c,b) by GTARSKI3:83;
then Line (c,b) = Line (a,b) by A3, A23, A12, GTARSKI3:87;
hence contradiction by A7, GTARSKI3:83; :: thesis: verum

end;

T23: a in Plane ((Line (c,b)),r999) by A1, A19, A14, A21, Th43;
A24: a in Line (a,b) by GTARSKI3:83;
A25: Line (a,b) <> Line (c,b) by GTARSKI3:83, A22;
( b in Line (a,b) & b in Line (c,b) ) by GTARSKI3:83;
then W1: not (Line (c,b)) /\ (Line (a,b)) is empty by XBOOLE_0:def 4;
A26: Line (a,b), Line (c,b) Is b by A12, A22, GTARSKI3:83;
consider s being POINT of S such that
A27: not s in Line (a,b) and
s in Line (c,b) and
A28: Plane ((Line (a,b)),(Line (c,b))) = Plane ((Line (a,b)),s) by A25, W1, A12, Def13;
J1: Line (a,b) is_line by A3;
j3: ( Line (c,b) c= Plane ((Line (a,b)),(Line (c,b))) & c in Line (c,b) ) by A26, Th43, GTARSKI3:83;
A30: E = Plane ((Line (c,b)),(Line (p,q))) by A19, A14, Th43
.= Plane ((Line (c,b)),a) by A21, A22, T1, A20, T23, Th34
.= Plane ((Line (c,b)),(Line (a,b))) by A22, W1, A24, A12, Def13
.= Plane ((Line (a,b)),(Line (c,b))) by A26, Th43
.= Plane ((Line (a,b)),c) by J1, A27, j3, A7, A28, Th34 ;
thus Line (a,b) c= E by A12, A7, A30, Th31; :: thesis: ex c being POINT of S st
( not Collinear a,b,c & E = Plane (a,b,c) )
A31: not Collinear a,b,c by A7;
take c ; :: thesis: ( not Collinear a,b,c & E = Plane (a,b,c) )
thus ( not Collinear a,b,c & E = Plane (a,b,c) ) by A31, A30, Def11; :: thesis: verum

end;

end;