A1: (MSVars C) . (a_Term C) = Vars by Def25;
C variables_in e c= MSVars C by MSAFREE3:27;
hence (C variables_in e) . (a_Term C) is Subset of Vars by A1; :: thesis: verum