theorem Satz5p5: :: GTARSKI3:59

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d being POINT of S holds
( a,b <= c,d iff ex x being POINT of S st
( between a,b,x & a,x equiv c,d ) )