let p, q be Element of CQC-WFF ; :: thesis: ( p |-| q iff {p} |-| {q} )

A1: now

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, Def5; :: thesis: verum

end;

now

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

end;

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