( (MSVars C) . (a_Term C) = Vars & C variables_in e c= MSVars C ) by MSVARS, MSAFREE3:28;
hence (C variables_in e) . (a_Term C) is Subset of Vars by PBOOLE:def 5; :: thesis: verum