theorem Th53: :: SPRECT_1:53

for p, q being Point of (TOP-REAL 2) st p `2 <= q `2 holds
proj2 .: (LSeg (p,q)) = [.(p `2),(q `2).]