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