theorem Th24: :: ORDINAL6:24

for X, Y being ordinal-membered set st ( for x, y being set st x in X & y in Y holds
x in y ) holds
(numbering X) ^ (numbering Y) is_isomorphism_of RelIncl ((ord-type X) +^ (ord-type Y)), RelIncl (X \/ Y)