let P be Subset of ; :: thesis: (SW-corner P) `2 = (SE-corner P) `2
thus (SW-corner P) `2 = S-bound P by EUCLID:56
.= (SE-corner P) `2 by EUCLID:56 ; :: thesis: verum