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