for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, p being POINT of S st p out a,b holds
( p,a <= p,b iff between p,a,b )