theorem :: ORDINAL3:17

for A, B, C, D being Ordinal st ( A c= B or A in B ) & C in D holds
A +^ C in B +^ D