ex a being ordinal number st X c= a by SS;
hence RelIncl X is well-ordering by WELLORD2:9; :: thesis: verum