dom R c= X by Def16;
hence R | X = R by Th62; :: thesis: verum