let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A st p <==> q holds
p |-| q
let p, q be Element of CQC-WFF A; :: thesis: ( p <==> q implies p |-| q )
assume p <==> q ; :: thesis: p |-| q
then p <=> q is valid ;
then (p => q) '&' (q => p) is valid by QC_LANG2:def 4;
then A1: {} (CQC-WFF A) |- (p => q) '&' (q => p) by CQC_THE1:def 9;
then {} (CQC-WFF A) |- q => p by Lm3;
then A2: q => p is valid by CQC_THE1:def 9;
{} (CQC-WFF A) |- 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