for A being Ordinal st A <> {} & A is limit_ordinal holds
for x being set holds
( x in Rank A iff ex B being Ordinal st
( B in A & x in Rank B ) )