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