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