theorem Th36: :: SUBSTUT1:36

for A being QC-alphabet
for S being Element of QC-Sub-WFF A st CQC_Sub S is Element of CQC-WFF A holds
CQC_Sub (Sub_not S) is Element of CQC-WFF A