S in CQC-Sub-WFF Al ;
then S in { S1 where S1 is Element of QC-Sub-WFF Al : S1 `1 is Element of CQC-WFF Al } by SUBSTUT1:def 39;
then ex S1 being Element of QC-Sub-WFF Al st
( S = S1 & S1 `1 is Element of CQC-WFF Al ) ;
hence S `1 is Element of CQC-WFF Al ; :: thesis: verum