theorem Th28: :: SUBSTUT1:28

for A being QC-alphabet
for S being Element of QC-Sub-WFF A st S is Sub_negative holds
CQC_Sub S = 'not' (CQC_Sub (Sub_the_argument_of S))