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

proof

assume a = c ; :: thesis: contradiction
then Collinear a,c,b by GTARSKI3:46;
hence contradiction by A1, GTARSKI3:14; :: thesis: verum

end;

A9: b <> c

proof

assume b = c ; :: thesis: contradiction
then Collinear b,c,a by GTARSKI3:46;
hence contradiction by A1; :: thesis: verum

end;

Plane (a,b,c) c= E

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Plane (a,b,c) or x in E )
assume A10: x in Plane (a,b,c) ; :: thesis: x in E
then reconsider d = x as POINT of S ;
a,b,c,d are_coplanar by A10, A2;
then consider y being POINT of S such that
A11: ( ( Collinear a,b,y & Collinear c,d,y ) or ( Collinear a,c,y & Collinear b,d,y ) or ( Collinear a,d,y & Collinear b,c,y ) ) by Th68;

per cases ( ( Collinear a,b,y & Collinear c,d,y ) or ( Collinear a,c,y & Collinear b,d,y ) or ( Collinear a,d,y & Collinear b,c,y ) ) by A11;

suppose A12: ( Collinear a,b,y & Collinear c,d,y ) ; :: thesis: x in E

then A13: y in Line (a,b) ;
A14: Line (a,b) c= E by A7, A3, A4, A6;
Collinear c,y,d by A12, GTARSKI3:14;
then A15: d in Line (c,y) ;
Line (c,y) c= E by A12, A1, A14, A13, A5, A6;
hence x in E by A15; :: thesis: verum

end;

suppose A16: ( Collinear a,c,y & Collinear b,d,y ) ; :: thesis: x in E

then A17: y in Line (a,c) ;
A18: Line (a,c) c= E by A8, A3, A5, A6;
Collinear b,y,d by A16, GTARSKI3:14;
then A19: d in Line (b,y) ;
b <> y by A16, A1, GTARSKI3:14;
then Line (b,y) c= E by A18, A17, A4, A6;
hence x in E by A19; :: thesis: verum

end;

suppose A20: ( Collinear a,d,y & Collinear b,c,y ) ; :: thesis: x in E

then A21: y in Line (b,c) ;
A22: Line (b,c) c= E by A9, A4, A5, A6;
Collinear a,y,d by A20, GTARSKI3:14;
then A23: d in Line (a,y) ;
Line (a,y) c= E by A20, A1, A22, A21, A3, A6;
hence x in E by A23; :: thesis: verum

end;

end;

end;

hence Plane (a,b,c) c= E ; :: thesis: verum