(NW-corner P) `1 = W-bound P by EUCLID:56
.= (SW-corner P) `1 by EUCLID:56 ;
hence LSeg ((NW-corner P),(SW-corner P)) is vertical by SPPOL_1:37; :: thesis: verum