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