(MSVars C) . a_Term = Vars by Def25;
then root-tree [x,a_Term] in QuasiTerms C by MSAFREE3:4;
hence root-tree [x,a_Term] is quasi-term of C by Th41; :: thesis: verum