ex A being Ordinal st rng phi c= A by ORDINAL2:def 8;
then On (rng phi) = rng phi by ORDINAL3:8;
hence Union phi is ordinal by ORDINAL3:7; :: thesis: verum