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

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