let p, q, r be Element of CQC-WFF ; :: thesis: ((p 'or' q) => r) => ((p => r) 'or' (q => r)) in TAUT
( q => (p 'or' q) in TAUT & (q => (p 'or' q)) => (((p 'or' q) => r) => (q => r)) in TAUT ) by Th4, LUKASI_1:1;
then ((p 'or' q) => r) => (q => r) in TAUT by CQC_THE1:46;
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