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