ex a being Ordinal st X c= a by Def1;
hence RelIncl X is well-ordering by WELLORD2:8; :: thesis: verum