let p, q be Element of CQC-WFF ; :: thesis: ( p <==> q iff ( p => q is valid & q => p is valid ) )

A1: now

assume that
A2: p => q is valid and
A3: q => p is valid ; :: thesis: p <==> q
A4: {} CQC-WFF |- q => p by A3, CQC_THE1:def 9;
{} CQC-WFF |- p => q by A2, CQC_THE1:def 9;
then {} CQC-WFF |- (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 by Def7; :: thesis: verum

end;

now

assume p <==> q ; :: thesis: ( p => q is valid & q => p is valid )
then p <=> q is valid by Def7;
then (p => q) '&' (q => p) is valid by QC_LANG2:def 4;
then A5: {} CQC-WFF |- (p => q) '&' (q => p) by CQC_THE1:def 9;
then A6: {} CQC-WFF |- q => p by Lm3;
{} CQC-WFF |- 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