(SW-corner P) `2 = S-bound P by EUCLID:56
.= (SE-corner P) `2 by EUCLID:56 ;
hence LSeg (SW-corner P),(SE-corner P) is horizontal by SPPOL_1:36; :: thesis: verum