let C be non empty compact Subset of (TOP-REAL 2); :: thesis: proj1 .: (LSeg ((SE-corner C),(SW-corner C))) = [.(W-bound C),(E-bound C).]
A1: (SW-corner C) `1 = W-bound C by EUCLID:52;
(SE-corner C) `1 = E-bound C by EUCLID:52;
hence proj1 .: (LSeg ((SE-corner C),(SW-corner C))) = [.(W-bound C),(E-bound C).] by A1, Th21, Th52; :: thesis: verum