consider A being Ordinal;
consider L being T-Sequence of ;
take L ; :: thesis: L is Ordinal-yielding
take A ; :: according to ORDINAL2:def 8 :: thesis: rng L c= A
thus rng L c= A by RELAT_1:def 19; :: thesis: verum