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