theorem Th16: :: SUBLEMMA:16

for Al being QC-alphabet
for S being Element of CQC-Sub-WFF Al holds
( (Sub_not S) `1 = 'not' (S `1) & (Sub_not S) `2 = S `2 )