let X, Y be non empty compact Subset of (TOP-REAL 2); :: thesis: ( E-bound X < E-bound Y implies E-min (X \/ Y) = E-min Y )
A1:
X \/ Y is compact
by COMPTS_1:19;
assume A2:
E-bound X < E-bound Y
; :: thesis: E-min (X \/ Y) = E-min Y
then A3:
E-bound (X \/ Y) = E-bound Y
by Th24;
A4:
( (E-min (X \/ Y)) `1 = E-bound (X \/ Y) & (E-min Y) `1 = E-bound Y )
by EUCLID:56;
A5:
Y c= X \/ Y
by XBOOLE_1:7;
E-min Y in Y
by SPRECT_1:16;
then
E-min Y in E-most (X \/ Y)
by A1, A3, A4, A5, SPRECT_2:17;
then A6:
(E-min (X \/ Y)) `2 <= (E-min Y) `2
by A1, PSCOMP_1:108;
A7:
E-min (X \/ Y) in X \/ Y
by A1, SPRECT_1:16;