let C be non empty compact Subset of (TOP-REAL 2); :: thesis: proj1 .: (LSeg (NW-corner C),(NE-corner C)) = [.(W-bound C),(E-bound C).]
( (NW-corner C) `1 = W-bound C & (NE-corner C) `1 = E-bound C ) by EUCLID:56;
hence proj1 .: (LSeg (NW-corner C),(NE-corner C)) = [.(W-bound C),(E-bound C).] by Th23, Th60; :: thesis: verum