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 A1: 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 ;
'not' (S `1) in CQC-WFF Al ;
then (Sub_not S) `1 in CQC-WFF Al by Th16;
hence Sub_not S is Element of CQC-Sub-WFF Al by A1; :: thesis: verum