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 by Th10;
hence p |- q by Def1; :: thesis: verum

end;

now

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

end;

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