let X, Y be non empty compact Subset of (TOP-REAL 2); :: thesis: ( X c= Y & N-max Y in X implies N-max X = N-max Y )
assume that
A1: X c= Y and
A2: N-max Y in X ; :: thesis: N-max X = N-max Y
A3: N-bound X <= N-bound Y by A1, PSCOMP_1:129;
A4: ( (N-max X) `2 = N-bound X & (N-max Y) `2 = N-bound Y ) by EUCLID:56;
A5: N-bound X >= (N-max Y) `2 by A2, PSCOMP_1:71;
then A6: N-bound X = N-bound Y by A3, A4, XXREAL_0:1;
N-max Y in N-most X by A2, A3, A4, A5, SPRECT_2:14, XXREAL_0:1;
then A7: (N-max X) `1 >= (N-max Y) `1 by PSCOMP_1:98;
N-max X in X by SPRECT_1:13;
then N-max X in N-most Y by A1, A3, A4, A5, SPRECT_2:14, XXREAL_0:1;
then (N-max X) `1 <= (N-max Y) `1 by PSCOMP_1:98;
then (N-max X) `1 = (N-max Y) `1 by A7, XXREAL_0:1;
hence N-max X = N-max Y by A4, A6, TOPREAL3:11; :: thesis: verum