let X be ordinal-membered set ; :: thesis: rng (numbering X) = X
thus rng (numbering X) = On X by Th18
.= X by Th2 ; :: thesis: verum