theorem Th59: :: ORDINAL5:59

for a, b, c being Ordinal st 0 in a & 1 in b & c = b -exponent a holds
a div^ (exp (b,c)) in b