:: deftheorem Def5 defines aleph CARD_1:def 5 :
for A being Ordinal
for b₂ being set holds
( b₂ = aleph A iff ex S being Sequence st
( b₂ = last S & dom S = succ A & S . 0 = card omega & ( for B being Ordinal st succ B in succ A holds
S . (succ B) = nextcard (S . B) ) & ( for B being Ordinal st B in succ A & B <> 0 & B is limit_ordinal holds
S . B = card (sup (S | B)) ) ) );