set q = the pure expression of C, a_Type C;
{} is finite Subset of (QuasiAdjs C) by XBOOLE_1:2;
then [{}, the pure expression of C, a_Type C] in { [A,t] where t is expression of C, a_Type C, A is finite Subset of (QuasiAdjs C) : t is pure } ;
hence not QuasiTypes C is empty ; :: thesis: verum