theorem :: PSCOMP_1:62
for P being Subset of (TOP-REAL 2) st N-max P = E-max P holds
N-max P = NE-corner P