theorem Th103: :: ORDINAL7:90
for a, b being non empty Ordinal holds
( omega *^ a c= b iff omega -exponent a in omega -exponent b )