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:57; :: thesis: verum