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).]
( (SW-corner C) `2 = S-bound C & (NW-corner C) `2 = N-bound C ) by EUCLID:56;
hence proj2 .: (LSeg (SW-corner C),(NW-corner C)) = [.(S-bound C),(N-bound C).] by Th24, Th61; :: thesis: verum