theorem Th71: :: SPRECT_1:71

for C being non empty compact Subset of (TOP-REAL 2) holds proj1 .: (LSeg ((NW-corner C),(NE-corner C))) = [.(W-bound C),(E-bound C).]