:: deftheorem Def6 defines Rank CLASSES1:def 6 :
for A being Ordinal
for b₂ being set holds
( b₂ = Rank A iff ex L being Sequence st
( b₂ = last L & dom L = succ A & L . 0 = {} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = bool (L . C) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
L . C = union (rng (L | C)) ) ) );