let U be Universe; :: thesis: U = Rank (On U)
card U = On U by Th9;
hence U = Rank (On U) by Th31; :: thesis: verum