let C be initialized ConstructorSignature; :: thesis: for t being ground pure expression of C, a_Type C holds ({} (QuasiAdjs C)) ast t is ground
let t be ground pure expression of C, a_Type C; :: thesis: ({} (QuasiAdjs C)) ast t is ground
set T = ({} (QuasiAdjs C)) ast t;
thus variables_in (({} (QuasiAdjs C)) ast t) = variables_in t by Th106
.= {} by Th107 ; :: according to ABCMIZ_1:def 50 :: thesis: verum