let p, q be Element of CQC-WFF ; :: thesis: ( p is_subformula_of p '&' q & q is_subformula_of p '&' q )
( p is_proper_subformula_of p '&' q & q is_proper_subformula_of p '&' q ) by QC_LANG2:89;
hence ( p is_subformula_of p '&' q & q is_subformula_of p '&' q ) by QC_LANG2:def 22; :: thesis: verum