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