theorem Th21: :: ORDINAL6:21

for X being set holds numbering X is_isomorphism_of RelIncl (ord-type X), RelIncl (On X)