consider t being ground pure expression of C, a_Type C;
take ({} (QuasiAdjs C)) ast t ; :: thesis: ({} (QuasiAdjs C)) ast t is ground
thus ({} (QuasiAdjs C)) ast t is ground ; :: thesis: verum