'not' (S `1 ) in CQC-WFF ;
then (Sub_not S) `1 in CQC-WFF by Th17;
then Sub_not S in CQC-Sub-WFF by SUBSTUT1:def 39;
hence Sub_not S is Element of CQC-Sub-WFF ; :: thesis: verum