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