let C be non empty compact Subset of (TOP-REAL 2); :: thesis: proj2 .: (LSeg ((SW-corner C),(NW-corner C))) = [.(S-bound C),(N-bound C).]
A1: (NW-corner C) `2 = N-bound C by EUCLID:52;
(SW-corner C) `2 = S-bound C by EUCLID:52;
hence proj2 .: (LSeg ((SW-corner C),(NW-corner C))) = [.(S-bound C),(N-bound C).] by A1, Th22, Th53; :: thesis: verum