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