now

let A be set ; :: thesis: ( A in ((MSVars C),(a_Term C) variables_in ) .: (adjs T) implies A is finite )
assume A in ((MSVars C),(a_Term C) variables_in ) .: (adjs T) ; :: thesis: A is finite
then consider x being set such that
A1: x in Union the Sorts of (Free C,(MSVars C)) and
x in adjs T and
A2: A = ((MSVars C),(a_Term C) variables_in ) . x by FUNCT_2:115;
reconsider x = x as expression of C by A1;
A = (C variables_in x) . (a_Term C) by A2, Def45;
hence A is finite ; :: thesis: verum

end;

then union (((MSVars C),(a_Term C) variables_in ) .: (adjs T)) is finite by FINSET_1:25;
hence variables_in T is finite ; :: thesis: verum