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 19;
( q is Element of CQC-WFF & r is Element of CQC-WFF ) by A1, CQC_LANG:19;
hence ex q, r being Element of CQC-WFF st p = q '&' r by A1; :: thesis: verum