Sub_& S1,S2 = [((S1 `1 ) '&' (S2 `1 )),(S1 `2 )] by A1, SUBSTUT1:def 21;
then (Sub_& S1,S2) `1 = (S1 `1 ) '&' (S2 `1 ) by MCART_1:7;
then consider S' being Element of QC-Sub-WFF such that
A2: ( Sub_& S1,S2 = S' & S' `1 is Element of CQC-WFF ) ;
Sub_& S1,S2 in CQC-Sub-WFF by A2, SUBSTUT1:def 39;
hence Sub_& S1,S2 is Element of CQC-Sub-WFF ; :: thesis: verum