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

A1: 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 {} CQC-WFF |- (p => q) '&' (q => p) by CQC_THE1:def 10;
then ( {} CQC-WFF |- p => q & {} CQC-WFF |- q => p ) by Lm3;
hence ( p => q is valid & q => p is valid ) by CQC_THE1:def 10; :: thesis: verum

end;

now

assume ( p => q is valid & q => p is valid ) ; :: thesis: p <==> q
then ( {} CQC-WFF |- p => q & {} CQC-WFF |- q => p ) by CQC_THE1:def 10;
then {} CQC-WFF |- (p => q) '&' (q => p) by Lm2;
then (p => q) '&' (q => p) is valid by CQC_THE1:def 10;
then p <=> q is valid by QC_LANG2:def 4;
hence p <==> q by Def7; :: thesis: verum

end;

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