theorem :: GTARSKI5:11

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b being POINT of S st a <> b holds
a out b,b by GTARSKI3:13;