let A be QC-alphabet ; :: thesis: for p being Element of CQC-WFF A st p is negative holds
ex q being Element of CQC-WFF A st p = 'not' q
let p be Element of CQC-WFF A; :: thesis: ( p is negative implies ex q being Element of CQC-WFF A st p = 'not' q )
assume p is negative ; :: thesis: ex q being Element of CQC-WFF A st p = 'not' q
then consider r being Element of QC-WFF A such that
A1: p = 'not' r by QC_LANG1:def 19;
r is Element of CQC-WFF A by A1, CQC_LANG:8;
hence ex q being Element of CQC-WFF A st p = 'not' q by A1; :: thesis: verum