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