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