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