let p, q, r be Element of CQC-WFF ; :: 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 9 :: thesis: {(p '&' q)} |- r
then r in Cn ({p} \/ {q}) by ENUMSET1:41;
hence r in Cn {(p '&' q)} by Th92; :: according to CQC_THE1:def 9 :: thesis: verum

end;

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