let X, Y be non empty compact Subset of (TOP-REAL 2); ( 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
; N-max X = N-max Y
A3:
N-bound X >= (N-max Y) `2
by A2, PSCOMP_1:24;
A4:
(N-max X) `2 = N-bound X
by EUCLID:52;
A5:
(N-max Y) `2 = N-bound Y
by EUCLID:52;
A6:
N-bound X <= N-bound Y
by A1, PSCOMP_1:66;
then A7:
N-bound X = N-bound Y
by A5, A3, XXREAL_0:1;
N-max Y in N-most X
by A2, A6, A5, A3, SPRECT_2:10, XXREAL_0:1;
then A8:
(N-max X) `1 >= (N-max Y) `1
by PSCOMP_1:39;
N-max X in X
by SPRECT_1:11;
then
N-max X in N-most Y
by A1, A6, A4, A5, A3, SPRECT_2:10, XXREAL_0:1;
then
(N-max X) `1 <= (N-max Y) `1
by PSCOMP_1:39;
then
(N-max X) `1 = (N-max Y) `1
by A8, XXREAL_0:1;
hence
N-max X = N-max Y
by A4, A5, A7, TOPREAL3:6; verum