for X being set
for A being Ordinal holds
( X c= Rank A iff X in Rank (succ A) )