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