theorem :: GTARSKI3:65

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c being POINT of S holds a,a <= b,c