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