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