let C be Subset of (TOP-REAL 2); :: thesis: LSeg (NW-corner C),(NE-corner C) is horizontal
(NW-corner C) `2 = N-bound C by EUCLID:56
.= (NE-corner C) `2 by EUCLID:56 ;
hence LSeg (NW-corner C),(NE-corner C) is horizontal by SPPOL_1:36; :: thesis: verum