let p be Element of CQC-WFF A; :: thesis: p <=> p is valid
{} (CQC-WFF A) |- p => p by CQC_THE1:def 9;
then {} (CQC-WFF A) |- (p => p) '&' (p => p) by Lm2;
then (p => p) '&' (p => p) is valid by CQC_THE1:def 9;
hence p <=> p is valid by QC_LANG2:def 4; :: thesis: verum