let p, q be Element of CQC-WFF ; :: thesis: ( p <==> q implies p |-| q )
assume p <==> q ; :: thesis: p |-| q
then p <=> q is valid by Def7;
then (p => q) '&' (q => p) is valid by QC_LANG2:def 4;
then A1: {} CQC-WFF |- (p => q) '&' (q => p) by CQC_THE1:def 9;
then {} CQC-WFF |- q => p by Lm3;
then A2: q => p is valid by CQC_THE1:def 9;
{} CQC-WFF |- p => q by A1, Lm3;
then p => q is valid by CQC_THE1:def 9;
hence ( p |- q & q |- p ) by A2, Th39; :: according to CQC_THE3:def 5 :: thesis: verum