ex p being Element of QC-WFF ex Sub being CQC_Substitution st S = [p,Sub] by SUBSTUT1:8;
hence S `2 is CQC_Substitution by MCART_1:7; :: thesis: verum