:: deftheorem Def9 defines the_rank_of CLASSES1:def 9 :
for X being set
for b₂ being Ordinal holds
( b₂ = the_rank_of X iff ( X c= Rank b₂ & ( for B being Ordinal st X c= Rank B holds
b₂ c= B ) ) );