theorem Th16: :: SUBSTUT2:16

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for Sub being CQC_Substitution of Al holds [('not' p),Sub] = Sub_not [p,Sub]