theorem Th24: :: ORDINAL5:24

for a being Ordinal
for m, n being Nat st 1 in a & m < n holds
a |^|^ m in a |^|^ n