'not' (S `1 ) in CQC-WFF ;
then (Sub_not S) `1 in CQC-WFF by Th17;
then consider S' being Element of QC-Sub-WFF such that
A1: ( Sub_not S = S' & S' `1 is Element of CQC-WFF ) ;
Sub_not S in CQC-Sub-WFF by A1, SUBSTUT1:def 39;
hence Sub_not S is Element of CQC-Sub-WFF ; :: thesis: verum