let A be QC-alphabet ; :: thesis: for p being Element of CQC-WFF A holds p <=> p is valid
let p be Element of CQC-WFF A; :: thesis: p <=> p is valid
(p => p) '&' (p => p) is valid by Lm8;
hence p <=> p is valid by QC_LANG2:def 4; :: thesis: verum