dom R c= X by Def18;
hence R | X = R by Th68; :: thesis: verum