set X = { G where G is Element of QC-Sub-WFF Al : G `1 is Element of CQC-WFF Al } ;
{ G where G is Element of QC-Sub-WFF Al : G `1 is Element of CQC-WFF Al } = CQC-Sub-WFF Al by SUBSTUT1:def 39;
then A2: for G being Element of QC-Sub-WFF Al st G `1 is Element of CQC-WFF Al holds
G in CQC-Sub-WFF Al ;
Sub_& (S1,S2) = [((S1 `1) '&' (S2 `1)),(S1 `2)] by A1, SUBSTUT1:def 21;
then (Sub_& (S1,S2)) `1 = (S1 `1) '&' (S2 `1) ;
hence Sub_& (S1,S2) is Element of CQC-Sub-WFF Al by A2; :: thesis: verum