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