for psi being Ordinal-Sequence holds Union psi is Ordinal ;