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