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