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 ;
All ((B `2),((B `1) `1)) in CQC-WFF Al ;
then (Sub_All (B,SQ)) `1 in CQC-WFF Al by A1, Th26;
hence Sub_All (B,SQ) is Element of CQC-Sub-WFF Al by A2; :: thesis: verum