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