let psi be Ordinal-Sequence; :: thesis: Union psi is Ordinal
ex A being Ordinal st rng psi c= A by ORDINAL2:def 8;
then ( Union psi = union (rng psi) & ( for x being set st x in rng psi holds
x is Ordinal ) ) by CARD_3:def 4;
hence Union psi is Ordinal by ORDINAL1:35; :: thesis: verum