let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A holds
( p <==> q iff ( p => q is valid & q => p is valid ) )
let p, q be Element of CQC-WFF A; :: thesis: ( p <==> q iff ( p => q is valid & q => p is valid ) )

A1: now :: thesis: ( p => q is valid & q => p is valid implies p <==> q )

assume that
A2: p => q is valid and
A3: q => p is valid ; :: thesis: p <==> q
A4: {} (CQC-WFF A) |- q => p by A3, CQC_THE1:def 9;
{} (CQC-WFF A) |- p => q by A2, CQC_THE1:def 9;
then {} (CQC-WFF A) |- (p => q) '&' (q => p) by A4, Lm2;
then (p => q) '&' (q => p) is valid by CQC_THE1:def 9;
then p <=> q is valid by QC_LANG2:def 4;
hence p <==> q ; :: thesis: verum

end;

now :: thesis: ( p <==> q implies ( p => q is valid & q => p is valid ) )

assume p <==> q ; :: thesis: ( p => q is valid & q => p is valid )
then p <=> q is valid ;
then (p => q) '&' (q => p) is valid by QC_LANG2:def 4;
then A5: {} (CQC-WFF A) |- (p => q) '&' (q => p) by CQC_THE1:def 9;
then A6: {} (CQC-WFF A) |- q => p by Lm3;
{} (CQC-WFF A) |- p => q by A5, Lm3;
hence ( p => q is valid & q => p is valid ) by A6, CQC_THE1:def 9; :: thesis: verum

end;

hence ( p <==> q iff ( p => q is valid & q => p is valid ) ) by A1; :: thesis: verum