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
( 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) ) )
let a, b, c be POINT of S; :: thesis: ( not Collinear a,b,c implies ( 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) ) ) )
assume not Collinear a,b,c ; :: thesis: ( 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) ) )
then ex E being Subset of S st
( Plane (a,b,c) = E & E is_plane & a in E & b in E & c in E ) by Th49;
hence ( 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 Th46; :: thesis: verum