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 T `1 is finite by MCART_1:7; :: thesis: verum