let p be Element of CQC-WFF ; :: thesis: p is_subformula_of 'not' p
p is_proper_subformula_of 'not' p by QC_LANG2:86;
hence p is_subformula_of 'not' p by QC_LANG2:def 22; :: thesis: verum