let U be Universe; :: thesis: U = Rank (On U)
( card U = On U & Rank (card U) = U ) by Th10, Th32;
hence U = Rank (On U) ; :: thesis: verum