:: deftheorem Def8 defines the_rank_of CLASSES1:def 8 :
for x being object
for b₂ being Ordinal holds
( b₂ = the_rank_of x iff ( x in Rank (succ b₂) & ( for B being Ordinal st x in Rank (succ B) holds
b₂ c= B ) ) );