theorem Th57: :: ORDINAL5:57

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