let A be QC-alphabet ; :: thesis: for r, s being Element of CQC-WFF A holds r <=> s is Element of CQC-WFF A
let r, s be Element of CQC-WFF A; :: thesis: r <=> s is Element of CQC-WFF A
r <=> s = (r => s) '&' (s => r) by QC_LANG2:def 4
.= ('not' (r '&' ('not' s))) '&' (s => r) by QC_LANG2:def 2
.= ('not' (r '&' ('not' s))) '&' ('not' (s '&' ('not' r))) by QC_LANG2:def 2 ;
hence r <=> s is Element of CQC-WFF A ; :: thesis: verum