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