consider q being pure expression of C, a_Type C;
{} is finite Subset of (QuasiAdjs C) by XBOOLE_1:2;
then [{} ,q] 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