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

A1: now

assume p |-| q ; :: thesis: {p} |-| {q}
then ( p |- q & q |- p ) by Def5;
then ( {p} |- {q} & {q} |- {p} ) by Th11;
hence {p} |-| {q} by Th18; :: thesis: verum

end;

now

assume {p} |-| {q} ; :: thesis: p |-| q
then ( {p} |- {q} & {q} |- {p} ) by Th18;
then ( p |- q & q |- p ) by Th11;
hence p |-| q by Def5; :: thesis: verum

end;

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