let q, r be Element of CQC-WFF ; :: thesis: ( q => (q => r) in TAUT implies q => r in TAUT )
(q => (q => r)) => (q => r) in TAUT by Th10;
hence ( q => (q => r) in TAUT implies q => r in TAUT ) by CQC_THE1:46; :: thesis: verum