let X, Y be non empty compact Subset of (TOP-REAL 2); ( 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
; 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; verum