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