theorem Th73: :: SPRECT_1:73

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