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