set R1 = RelIncl (ord-type X);
set R2 = RelIncl (On X);
set f = canonical_isomorphism_of ((RelIncl (ord-type X)),(RelIncl (On X)));
consider a being Ordinal such that
A1: On X c= a by Def1;
ex phi being Ordinal-Sequence st
( phi = canonical_isomorphism_of ((RelIncl (ord-type X)),(RelIncl (On X))) & phi is increasing & dom phi = ord-type X & rng phi = On X ) by A1, CARD_5:5;
hence numbering X is increasing ; :: thesis: verum