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