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
ex E being Subset of S st
( Plane (a,b,c) = E & E is_plane & a in E & b in E & c in E )
let a, b, c be POINT of S; :: thesis: ( not Collinear a,b,c implies ex E being Subset of S st
( Plane (a,b,c) = E & E is_plane & a in E & b in E & c in E ) )
assume A1: not Collinear a,b,c ; :: thesis: ex E being Subset of S st
( Plane (a,b,c) = E & E is_plane & a in E & b in E & c in E )
set E = Plane (a,b,c);
A2: Plane (a,b,c) = Plane ((Line (a,b)),c) by A1, Def11;
take Plane (a,b,c) ; :: thesis: ( Plane (a,b,c) = Plane (a,b,c) & Plane (a,b,c) is_plane & a in Plane (a,b,c) & b in Plane (a,b,c) & c in Plane (a,b,c) )
a <> b by A1, GTARSKI3:46;
then A3: Line (a,b) is_line ;
A4: not c in Line (a,b)

proof

assume c in Line (a,b) ; :: thesis: contradiction
then ex x being POINT of S st
( c = x & Collinear a,b,x ) ;
hence contradiction by A1; :: thesis: verum

end;

Line (a,b) c= Plane (a,b,c) by A3, A4, A2, Th31;
hence ( Plane (a,b,c) = Plane (a,b,c) & Plane (a,b,c) is_plane & a in Plane (a,b,c) & b in Plane (a,b,c) & c in Plane (a,b,c) ) by A1, A2, A3, Th48, GTARSKI3:83; :: thesis: verum