theorem Th41: :: GTARSKI5:41

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
ex r being POINT of S st
( not r in A & r in A9 & Plane (A,A9) = Plane (A,r) & A9 = Line (r,p) & ex r9 being POINT of S st
( between r,p,r9 & p <> r9 & Collinear r,p,r9 & not r9 in A & Plane (A,r) = Plane (A,r9) ) )