let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A holds
( p is_subformula_of p '&' q & q is_subformula_of p '&' q )
let p, q be Element of CQC-WFF A; :: thesis: ( p is_subformula_of p '&' q & q is_subformula_of p '&' q )
A1: q is_proper_subformula_of p '&' q by QC_LANG2:69;
p is_proper_subformula_of p '&' q by QC_LANG2:69;
hence ( p is_subformula_of p '&' q & q is_subformula_of p '&' q ) by A1, QC_LANG2:def 21; :: thesis: verum