:: deftheorem defines <= GTARSKI3:def 7 :
for S being TarskiGeometryStruct
for a, b, c, d being POINT of S holds
( a,b <= c,d iff ex y being POINT of S st
( between c,y,d & a,b equiv c,y ) );