ex a being Ordinal st X c= a by Def1;
hence union X is ordinal by ORDINAL3:4; :: thesis: verum