:: deftheorem defines is_space3 GTARSKI5:def 22 :
for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for E being Subset of S holds
( E is_space3 iff ex r being POINT of S ex A being Subset of S st
( A is_plane & not r in A & E = space3 (A,r) ) );