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