:: deftheorem Def13 defines Plane GTARSKI5:def 13 :
for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for A, A9 being Subset of S st A is_line & A9 is_line & A <> A9 & not A /\ A9 is empty holds
for b₄ being Subset of S holds
( b₄ = Plane (A,A9) iff ex r being POINT of S st
( not r in A & r in A9 & b₄ = Plane (A,r) ) );