:: deftheorem defines numbering ORDINAL6:def 6 :
for X being set holds numbering X = canonical_isomorphism_of ((RelIncl (ord-type X)),(RelIncl (On X)));