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