let X, Y be non empty compact Subset of (TOP-REAL 2); ( E-bound X < E-bound Y implies E-min (X \/ Y) = E-min Y )
A1:
(E-min (X \/ Y)) `1 = E-bound (X \/ Y)
by EUCLID:52;
A2:
X \/ Y is compact
by COMPTS_1:10;
then A3:
E-min (X \/ Y) in X \/ Y
by SPRECT_1:14;
A4:
E-min Y in Y
by SPRECT_1:14;
A5:
(E-min Y) `1 = E-bound Y
by EUCLID:52;
assume A6:
E-bound X < E-bound Y
; E-min (X \/ Y) = E-min Y
then A7:
E-bound (X \/ Y) = E-bound Y
by Th24;
Y c= X \/ Y
by XBOOLE_1:7;
then
E-min Y in E-most (X \/ Y)
by A2, A7, A5, A4, SPRECT_2:13;
then A8:
(E-min (X \/ Y)) `2 <= (E-min Y) `2
by A2, PSCOMP_1:47;