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