let p, q be Element of CQC-WFF ; :: thesis: ( p <=> q is valid implies q <=> p is valid )
assume p <=> q is valid ; :: thesis: q <=> p is valid
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;
then {} CQC-WFF |- (q => p) '&' (p => q) by Lm2;
then (q => p) '&' (p => q) is valid by CQC_THE1:def 10;
hence q <=> p is valid by QC_LANG2:def 4; :: thesis: verum