A1: ((MSVars C),(a_Term C) variables_in ) .: (adjs T) is Subset of (bool Vars ) by Def25;
union (bool Vars ) = Vars by ZFMISC_1:99;
then union (((MSVars C),(a_Term C) variables_in ) .: (adjs T)) c= Vars by A1, ZFMISC_1:95;
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