theorem :: GTARSKI5:57

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b being POINT of S
for A being Subset of S st between a,A,b holds
a <> b by GTARSKI1:def 10;