A1: (((MSVars C),(a_Term C)) variables_in) .: (adjs T) is Subset of (bool Vars) by Def25;
union (bool Vars) = Vars by ZFMISC_1:81;
then union ((((MSVars C),(a_Term C)) variables_in) .: (adjs T)) c= Vars by A1, ZFMISC_1:77;
hence (union ((((MSVars C),(a_Term C)) variables_in) .: (adjs T))) \/ (variables_in (the_base_of T)) is Subset of Vars by XBOOLE_1:8; :: thesis: verum