let p, q be Element of CQC-WFF A; :: 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 A) |- (p => q) '&' (q => p) by CQC_THE1:def 9;
then A2: {} (CQC-WFF A) |- q => p by Lm3;
{} (CQC-WFF A) |- p => q by A1, Lm3;
then {} (CQC-WFF A) |- (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