theorem :: ORDINAL6:26

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
ord-type (X \/ Y) = (ord-type X) +^ (ord-type Y)