let A be QC-alphabet ; :: thesis: for p, q, r being Element of CQC-WFF A holds ((p 'or' r) '&' (q 'or' r)) => ((p '&' q) 'or' r) in TAUT A
let p, q, r be Element of CQC-WFF A; :: thesis: ((p 'or' r) '&' (q 'or' r)) => ((p '&' q) 'or' r) in TAUT A
((('not' p) => r) '&' (('not' q) => r)) => ((('not' p) 'or' ('not' q)) => r) in TAUT A by Th36;
then ((p 'or' r) '&' (('not' q) => r)) => ((('not' p) 'or' ('not' q)) => r) in TAUT A by Lm1;
then A1: ((p 'or' r) '&' (q 'or' r)) => ((('not' p) 'or' ('not' q)) => r) in TAUT A by Lm1;
( ('not' (p '&' q)) => (('not' p) 'or' ('not' q)) in TAUT A & (('not' (p '&' q)) => (('not' p) 'or' ('not' q))) => (((('not' p) 'or' ('not' q)) => r) => (('not' (p '&' q)) => r)) in TAUT A ) by Th17, LUKASI_1:1;
then ((('not' p) 'or' ('not' q)) => r) => (('not' (p '&' q)) => r) in TAUT A by CQC_THE1:46;
then ((p 'or' r) '&' (q 'or' r)) => (('not' (p '&' q)) => r) in TAUT A by A1, LUKASI_1:3;
hence ((p 'or' r) '&' (q 'or' r)) => ((p '&' q) 'or' r) in TAUT A by Lm1; :: thesis: verum