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