for x, y being object holds not [x,y] in {} ~ by Def5;
hence X ~ is empty by Th31; :: thesis: verum