theorem :: JORDAN1J:28
for X, Y being non empty compact Subset of (TOP-REAL 2) st N-bound X < N-bound Y holds
N-max (X \/ Y) = N-max Y