Description: Define the rank function. See rankval , rankval2 , rankval3 , or
rankval4 its value. The rank is a kind of "inverse" of the cumulative
hierarchy of sets function R1 : given a set, it returns an ordinal
number telling us the smallest layer of the hierarchy to which the set
belongs. Based on Definition 9.14 of TakeutiZaring p. 79. Theorem
rankid illustrates the "inverse" concept. Another nice theorem
showing the relationship is rankr1a . (Contributed by NM, 11-Oct-2003)