ex A being finite Subset of ex q being pure expression of C, a_Type C st T = [A,q] by Th72;
hence vars T is Subset of by MCART_1:7; :: thesis: verum