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