theorem Th57: :: SPRECT_1:57

for p, q being Point of (TOP-REAL 2) st p `1 <= q `1 holds
E-bound (LSeg (p,q)) = q `1