let P be Subset of (TOP-REAL 2); :: thesis: (SE-corner P) `1 = (NE-corner P) `1
thus (SE-corner P) `1 = E-bound P by EUCLID:56
.= (NE-corner P) `1 by EUCLID:56 ; :: thesis: verum