for x, y being set holds not [x,y] in {} ~ by Def7;
hence X ~ is empty by Th56; :: thesis: verum