theorem Th10: :: CQC_SIM1:10
for A being QC-alphabet
for p being Element of CQC-WFF A holds p is_subformula_of 'not' p