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