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