let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for a, b, c being POINT of S
for E being Subset of S st not Collinear a,b,c & E is_plane & a in E & b in E & c in E holds
E = Plane (a,b,c)
let a, b, c be POINT of S; :: thesis: for E being Subset of S st not Collinear a,b,c & E is_plane & a in E & b in E & c in E holds
E = Plane (a,b,c)
let E be Subset of S; :: thesis: ( not Collinear a,b,c & E is_plane & a in E & b in E & c in E implies E = Plane (a,b,c) )
assume that
A1: not Collinear a,b,c and
A2: E is_plane and
A3: a in E and
A4: b in E and
A5: c in E ; :: thesis: E = Plane (a,b,c)
set A = Line (a,b);
A6: a <> b by A1, GTARSKI3:46;
then consider r being POINT of S such that
A7: not Collinear a,b,r and
A8: E = Plane (a,b,r) by A2, A3, A4, Th46;
A9: 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;

H1: Line (a,b) is_line by A6;
H2: not r in Line (a,b)

proof

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

end;

c in Plane ((Line (a,b)),r) by A5, A7, A8, Def11;
then Plane ((Line (a,b)),c) = Plane ((Line (a,b)),r) by Th34, H1, H2, A9
.= E by A7, A8, Def11 ;
hence E = Plane (a,b,c) by Def11, A1; :: thesis: verum