let X, Y be non empty compact Subset of (TOP-REAL 2); :: thesis: ( 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 ; :: thesis: E-min X = E-min Y
A3: E-bound X <= E-bound Y by A1, PSCOMP_1:130;
A4: ( (E-min X) `1 = E-bound X & (E-min Y) `1 = E-bound Y ) by EUCLID:56;
A5: E-bound X >= (E-min Y) `1 by A2, PSCOMP_1:71;
then A6: E-bound X = E-bound Y by A3, A4, XXREAL_0:1;
E-min Y in E-most X by A2, A3, A4, A5, SPRECT_2:17, XXREAL_0:1;
then A7: (E-min X) `2 <= (E-min Y) `2 by PSCOMP_1:108;
E-min X in X by SPRECT_1:16;
then E-min X in E-most Y by A1, A3, A4, A5, SPRECT_2:17, XXREAL_0:1;
then (E-min X) `2 >= (E-min Y) `2 by PSCOMP_1:108;
then (E-min X) `2 = (E-min Y) `2 by A7, XXREAL_0:1;
hence E-min X = E-min Y by A4, A6, TOPREAL3:11; :: thesis: verum