(NW-corner C) `2 = N-bound C by EUCLID:52
.= (NE-corner C) `2 by EUCLID:52 ;
hence LSeg ((NW-corner C),(NE-corner C)) is horizontal by SPPOL_1:15; :: thesis: verum