let X, Y be non empty compact Subset of (TOP-REAL 2); :: thesis: ( E-bound X <= E-bound Y implies E-bound (X \/ Y) = E-bound Y )
assume E-bound X <= E-bound Y ; :: thesis: E-bound (X \/ Y) = E-bound Y
then max ((E-bound X),(E-bound Y)) = E-bound Y by XXREAL_0:def 10;
hence E-bound (X \/ Y) = E-bound Y by SPRECT_1:50; :: thesis: verum