for S being satisfying_Tarski-model TarskiGeometryStruct
for p, a, b being POINT of S st p out a,b & p,a <= p,b holds
between p,a,b by Satz6p13;