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