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