let x be set ; :: according to ORDINAL6:def 9 :: thesis: ( x in rng (g | X) implies x is Ordinal-Sequence )
rng (g | X) c= rng g by RELAT_1:70;
hence ( x in rng (g | X) implies x is Ordinal-Sequence ) by Def9; :: thesis: verum