theorem Th70: :: SPRECT_1:70

for C being non empty compact Subset of (TOP-REAL 2) holds proj2 .: (LSeg ((SW-corner C),(NW-corner C))) = [.(S-bound C),(N-bound C).]