theorem :: ORDINAL7:6

for a, b being Ordinal st 1 in a & a in b holds
exp (b,a) in b |^|^ a