theorem Th30: :: ORDINAL7:17

for a, b being Ordinal holds
( a +^ b = b iff omega *^ a c= b )