let X, Y be non empty compact Subset of (TOP-REAL 2); :: thesis: ( 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 ; :: thesis: E-max X = E-max Y
A3: E-bound X <= E-bound Y by A1, PSCOMP_1:130;
A4: ( (E-max X) `1 = E-bound X & (E-max Y) `1 = E-bound Y ) by EUCLID:56;
A5: E-bound X >= (E-max Y) `1 by A2, PSCOMP_1:71;
then A6: E-bound X = E-bound Y by A3, A4, XXREAL_0:1;
E-max Y in E-most X by A2, A3, A4, A5, SPRECT_2:17, XXREAL_0:1;
then A7: (E-max X) `2 >= (E-max Y) `2 by PSCOMP_1:108;
E-max X in X by SPRECT_1:16;
then E-max X in E-most Y by A1, A3, A4, A5, SPRECT_2:17, XXREAL_0:1;
then (E-max X) `2 <= (E-max Y) `2 by PSCOMP_1:108;
then (E-max X) `2 = (E-max Y) `2 by A7, XXREAL_0:1;
hence E-max X = E-max Y by A4, A6, TOPREAL3:11; :: thesis: verum