:: deftheorem Def13 defines rank_univers CLASSES4:def 13 :
for X being Element of union (rng sequence_univers)
for b₂ being Nat holds
( b₂ = rank_univers X iff ( X in sequence_univers . b₂ & ( for n being Nat st n < b₂ holds
not X in sequence_univers . n ) ) );