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