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
A2: ( x in Union the Sorts of (Free C,(MSVars C)) & x in adjs T & A = ((MSVars C),(a_Term C) variables_in ) . x ) by FUNCT_2:115;
reconsider x = x as expression of C by A2;
A = (C variables_in x) . (a_Term C) by A2, VARS'INF;
hence A is finite ; :: thesis: verum

end;

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