let p, q, r be Element of CQC-WFF ; :: thesis: ((p 'or' q) => r) => ((p => r) 'or' (q => r)) in TAUT
A1: q => (p 'or' q) in TAUT by Th4;
(q => (p 'or' q)) => (((p 'or' q) => r) => (q => r)) in TAUT by LUKASI_1:1;
then ((p 'or' q) => r) => (q => r) in TAUT by A1, CQC_THE1:82;
then ('not' (p => r)) => (((p 'or' q) => r) => (q => r)) in TAUT by LUKASI_1:13;
then ((p 'or' q) => r) => (('not' (p => r)) => (q => r)) in TAUT by LUKASI_1:15;
hence ((p 'or' q) => r) => ((p => r) 'or' (q => r)) in TAUT by Lm1; :: thesis: verum