theorem :: GTARSKI5:35

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for p, q being POINT of S
for A, A9 being Subset of S st A,A9 Is p & A,A9 Is q holds
p = q by GTARSKI3:89;