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 A2: {p} |-| {q} ; :: thesis: p |-| q
then {q} |- {p} by Th18;
then A3: q |- p by Th11;
{p} |- {q} by A2, Th18;
then p |- q by Th11;
hence p |-| q by A3; :: thesis: verum

end;

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

assume A4: p |-| q ; :: thesis: {p} |-| {q}
then q |- p ;
then A5: {q} |- {p} by Th11;
p |- q by A4;
then {p} |- {q} by Th11;
hence {p} |-| {q} by A5, Th18; :: thesis: verum

end;

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