let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A holds {p,q} |-| {(p '&' q)}
let p, q be Element of CQC-WFF A; :: thesis: {p,q} |-| {(p '&' q)}
for r being Element of CQC-WFF A holds
( {p,q} |- r iff {(p '&' q)} |- r ) by CQC_THE2:89;
hence {p,q} |-| {(p '&' q)} by Def4; :: thesis: verum