set a = the Element of X;
[ the Element of X, the Element of X] in RelIncl X by Def1;
hence not RelIncl X is empty ; :: thesis: verum