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