theorem Th40: :: ORDINAL7:27

for a1, a2, b being Ordinal st a1 in exp (omega,b) & a2 in exp (omega,b) holds
a1 +^ a2 in exp (omega,b)