for a, b being Ordinal st omega -exponent a in omega -exponent b holds
a in exp (omega,(omega -exponent b))