let A be QC-alphabet ; :: thesis: for p being Element of CQC-WFF A holds p is_subformula_of 'not' p
let p be Element of CQC-WFF A; :: thesis: p is_subformula_of 'not' p
p is_proper_subformula_of 'not' p by QC_LANG2:66;
hence p is_subformula_of 'not' p by QC_LANG2:def 21; :: thesis: verum