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