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