let psi be Ordinal-Sequence; :: thesis: Union psi is Ordinal
consider A being Ordinal such that
A1: rng psi c= A by ORDINAL2:def 8;
A2: Union psi = union (rng psi) by CARD_3:def 4;
for x being set st x in rng psi holds
x is Ordinal by A1;
hence Union psi is Ordinal by A2, ORDINAL1:35; :: thesis: verum