theorem Th40: :: GTARSKI5:40

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 (A9,A) & A9 c= Plane (A,A9) )