:: deftheorem Def10 defines Plane GTARSKI5:def 10 :
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_line & not r in A holds
for b₄ being Subset of S holds
( b₄ = Plane (A,r) iff ex r9 being POINT of S st
( between r,A,r9 & b₄ = ((half-plane (A,r)) \/ A) \/ (half-plane (A,r9)) ) );