theorem Th69: :: CARD_2:70

for A being Ordinal holds
( A is limit_ordinal iff for B being Ordinal
for n being Nat st B in A holds
B +^ n in A )