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

proof

assume for c being POINT of S holds
( c in Line (a,b) or not c in Line (p,q) ) ; :: thesis: contradiction
then ( Line (a,b) is_line & p <> q & p in Line (p,q) & q in Line (p,q) & p in Line (a,b) & q in Line (a,b) ) by A3, A4, GTARSKI3:46, GTARSKI3:83;
hence contradiction by A7, GTARSKI3:87; :: thesis: verum

end;

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