theorem :: ORDINAL6:20

for X being set holds card (dom (numbering X)) = card (On X)