theorem Th18: :: ORDINAL6:18

for X being set holds
( dom (numbering X) = ord-type X & rng (numbering X) = On X )