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

A1: now :: thesis: ( p |- q implies {p} |- {q} )

assume p |- q ; :: thesis: {p} |- {q}
then {p} |- q by Def1;
hence {p} |- {q} by Th10; :: thesis: verum

end;

now :: thesis: ( {p} |- {q} implies p |- q )

assume {p} |- {q} ; :: thesis: p |- q
then {p} |- q by Th10;
hence p |- q by Def1; :: thesis: verum

end;

hence ( {p} |- {q} iff p |- q ) by A1; :: thesis: verum