theorem :: GTARSKI5:71

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 between2 a,A,b holds
between2 b,A,a by GTARSKI3:14;