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