rng (R | A) c= rng R by Th64;
hence R | A is non-empty by Def7; :: thesis: verum