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