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