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