let A be QC-alphabet ; :: thesis: for q, r being Element of CQC-WFF A st q => (q => r) in TAUT A holds
q => r in TAUT A
let q, r be Element of CQC-WFF A; :: thesis: ( q => (q => r) in TAUT A implies q => r in TAUT A )
(q => (q => r)) => (q => r) in TAUT A by Th10;
hence ( q => (q => r) in TAUT A implies q => r in TAUT A ) by CQC_THE1:46; :: thesis: verum