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