theorem Th24: :: ORDINAL4:24
for A, B, C being Ordinal st 1 in C & A in B holds
exp (C,A) in exp (C,B)