let X be set ; :: thesis: numbering X is_isomorphism_of RelIncl (ord-type X), RelIncl (On X)
set R1 = RelIncl (ord-type X);
set R2 = RelIncl (On X);
RelIncl (On X), RelIncl (ord-type X) are_isomorphic by WELLORD2:def 2;
then RelIncl (ord-type X), RelIncl (On X) are_isomorphic by WELLORD1:40;
hence numbering X is_isomorphism_of RelIncl (ord-type X), RelIncl (On X) by WELLORD1:def 9; :: thesis: verum