(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