let P be Subset of (TOP-REAL 2); :: thesis: ( E-min P = S-max P implies E-min P = SE-corner P )
assume A1: E-min P = S-max P ; :: thesis: E-min P = SE-corner P
( (E-min P) `1 = E-bound P & (S-max P) `2 = S-bound P & (SE-corner P) `1 = E-bound P & (SE-corner P) `2 = S-bound P ) by EUCLID:56;
hence E-min P = SE-corner P by A1, EUCLID:57; :: thesis: verum