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