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