let P be Subset of (TOP-REAL 2); :: thesis: (SW-corner P) `1 = (NW-corner P) `1
thus (SW-corner P) `1 = W-bound P by EUCLID:52
.= (NW-corner P) `1 by EUCLID:52 ; :: thesis: verum