theorem :: PSCOMP_1:61

for P being Subset of (TOP-REAL 2) st W-max P = N-min P holds
W-max P = NW-corner P