theorem Th23: :: ORDINAL4:23
for A, C being Ordinal st 1 in C holds
exp (C,A) in exp (C,(succ A))