for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for c, a1, a2, b1, b2, m1, m2 being POINT of S st between a1,c,a2 & between b1,c,b2 & c,a1 equiv c,b1 & c,a2 equiv c,b2 & Middle a1,m1,b1 & Middle a2,m2,b2 & c,a2 <= c,a1 holds
between m1,c,m2