:: deftheorem Def20 defines space3 GTARSKI5:def 20 :
for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for A being Subset of S
for r being POINT of S st A is_plane & not r in A holds
for b₄ being Subset of S holds
( b₄ = space3 (A,r) iff ex r9 being POINT of S st
( between2 r,A,r9 & b₄ = ((half-space3 (A,r)) \/ A) \/ (half-space3 (A,r9)) ) );