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