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