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).]
A1: (NE-corner C) `1 = E-bound C by EUCLID:56;
(NW-corner C) `1 = W-bound C by EUCLID:56;
hence proj1 .: (LSeg (NW-corner C),(NE-corner C)) = [.(W-bound C),(E-bound C).] by A1, Th23, Th60; :: thesis: verum