for x, y being set holds not [x,y] in X | R by Def12;
hence X | R is empty by Th56; :: thesis: verum