theorem Th23: :: ORDINAL7:10
for a, b, c being Ordinal st 0 in a & 1 in b & a in exp (b,c) holds
b -exponent a in c