let A be QC-alphabet ; :: thesis: for p, q, r being Element of CQC-WFF A holds
( {p,q} |- r iff {(p '&' q)} |- r )
let p, q, r be Element of CQC-WFF A; :: thesis: ( {p,q} |- r iff {(p '&' q)} |- r )
thus ( {p,q} |- r implies {(p '&' q)} |- r ) :: thesis: ( {(p '&' q)} |- r implies {p,q} |- r )

proof

assume r in Cn {p,q} ; :: according to CQC_THE1:def 8 :: thesis: {(p '&' q)} |- r
then r in Cn ({p} \/ {q}) by ENUMSET1:1;
hence r in Cn {(p '&' q)} by Th88; :: according to CQC_THE1:def 8 :: thesis: verum

end;

assume r in Cn {(p '&' q)} ; :: according to CQC_THE1:def 8 :: thesis: {p,q} |- r
then r in Cn ({p} \/ {q}) by Th88;
hence r in Cn {p,q} by ENUMSET1:1; :: according to CQC_THE1:def 8 :: thesis: verum