let p, q be Element of CQC-WFF ; :: thesis: (p => q) => ((q => p) => (p <=> q)) in TAUT
(p => q) => ((q => p) => ((p => q) '&' (q => p))) in TAUT by Th28;
hence (p => q) => ((q => p) => (p <=> q)) in TAUT by QC_LANG2:def 4; :: thesis: verum