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