let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for E being Subset of S st E is_space3 holds
ex a, b, c, d being POINT of S st
( not a,b,c,d are_coplanar & E = space3 (a,b,c,d) )
let E be Subset of S; :: thesis: ( E is_space3 implies ex a, b, c, d being POINT of S st
( not a,b,c,d are_coplanar & E = space3 (a,b,c,d) ) )
assume E is_space3 ; :: thesis: ex a, b, c, d being POINT of S st
( not a,b,c,d are_coplanar & E = space3 (a,b,c,d) )
then consider r being POINT of S, A being Subset of S such that
A1: A is_plane and
A2: not r in A and
A3: E = space3 (A,r) ;
consider a, b, c being POINT of S such that
A4: not Collinear a,b,c and
A5: A = Plane (a,b,c) by A1;
take a ; :: thesis: ex b, c, d being POINT of S st
( not a,b,c,d are_coplanar & E = space3 (a,b,c,d) )
take b ; :: thesis: ex c, d being POINT of S st
( not a,b,c,d are_coplanar & E = space3 (a,b,c,d) )
take c ; :: thesis: ex d being POINT of S st
( not a,b,c,d are_coplanar & E = space3 (a,b,c,d) )
take r ; :: thesis: ( not a,b,c,r are_coplanar & E = space3 (a,b,c,r) )
( a in A & b in A & c in A ) by A4, A5, Th69;
hence ( not a,b,c,r are_coplanar & E = space3 (a,b,c,r) ) by A5, A3, Def21, A1, A2, A4, Th87; :: thesis: verum