theorem :: JORDAN1J:29
for X, Y being non empty compact Subset of (TOP-REAL 2) st E-bound X < E-bound Y holds
E-min (X \/ Y) = E-min Y