theorem Th29: :: SUBSTUT1:29

for A being QC-alphabet
for S being Element of QC-Sub-WFF A holds CQC_Sub (Sub_not S) = 'not' (CQC_Sub S)