theorem :: GTARSKI3:62

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d, e, f being POINT of S st a,b <= c,d & c,d <= e,f holds
a,b <= e,f