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