theorem Th43: :: GTARSKI5:43

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for p being POINT of S
for A, A9 being Subset of S st A,A9 Is p holds
( A c= Plane (A,A9) & A9 c= Plane (A,A9) & Plane (A,A9) = Plane (A9,A) )