let X, Y be non empty compact Subset of (TOP-REAL 2); ( X c= Y & E-max Y in X implies E-max X = E-max Y )
assume that
A1:
X c= Y
and
A2:
E-max Y in X
; E-max X = E-max Y
A3:
E-bound X >= (E-max Y) `1
by A2, PSCOMP_1:24;
A4:
(E-max X) `1 = E-bound X
by EUCLID:52;
A5:
(E-max Y) `1 = E-bound Y
by EUCLID:52;
A6:
E-bound X <= E-bound Y
by A1, PSCOMP_1:67;
then A7:
E-bound X = E-bound Y
by A5, A3, XXREAL_0:1;
E-max Y in E-most X
by A2, A6, A5, A3, SPRECT_2:13, XXREAL_0:1;
then A8:
(E-max X) `2 >= (E-max Y) `2
by PSCOMP_1:47;
E-max X in X
by SPRECT_1:14;
then
E-max X in E-most Y
by A1, A6, A4, A5, A3, SPRECT_2:13, XXREAL_0:1;
then
(E-max X) `2 <= (E-max Y) `2
by PSCOMP_1:47;
then
(E-max X) `2 = (E-max Y) `2
by A8, XXREAL_0:1;
hence
E-max X = E-max Y
by A4, A5, A7, TOPREAL3:6; verum