consider a being Element of X;
[a,a] in RelIncl X by WELLORD2:def 1;
hence not RelIncl X is empty ; :: thesis: verum