let p, q, r be Element of CQC-WFF ; :: thesis: ((p 'or' q) '&' r) => ((p '&' r) 'or' (q '&' r)) in TAUT
A1: ('not' ((('not' p) 'or' ('not' r)) '&' (('not' q) 'or' ('not' r)))) => (('not' (('not' p) 'or' ('not' r))) 'or' ('not' (('not' q) 'or' ('not' r)))) in TAUT by Th17;
((('not' p) 'or' ('not' r)) '&' (('not' q) 'or' ('not' r))) => ((('not' p) '&' ('not' q)) 'or' ('not' r)) in TAUT by Th40;
then A2: ('not' ((('not' p) '&' ('not' q)) 'or' ('not' r))) => ('not' ((('not' p) 'or' ('not' r)) '&' (('not' q) 'or' ('not' r)))) in TAUT by LUKASI_1:34;
(('not' (('not' p) '&' ('not' q))) '&' ('not' ('not' r))) => ('not' ((('not' p) '&' ('not' q)) 'or' ('not' r))) in TAUT by Th7;
then (('not' (('not' p) '&' ('not' q))) '&' ('not' ('not' r))) => ('not' ((('not' p) 'or' ('not' r)) '&' (('not' q) 'or' ('not' r)))) in TAUT by A2, LUKASI_1:3;
then A3: ((p 'or' q) '&' ('not' ('not' r))) => ('not' ((('not' p) 'or' ('not' r)) '&' (('not' q) 'or' ('not' r)))) in TAUT by QC_LANG2:def 3;
( ('not' (p '&' r)) => (('not' p) 'or' ('not' r)) in TAUT & (('not' (p '&' r)) => (('not' p) 'or' ('not' r))) => (('not' (('not' p) 'or' ('not' r))) => (p '&' r)) in TAUT ) by Th17, LUKASI_1:31;
then ('not' (('not' p) 'or' ('not' r))) => (p '&' r) in TAUT by CQC_THE1:46;
then A4: (('not' (('not' p) 'or' ('not' r))) 'or' ('not' (('not' q) 'or' ('not' r)))) => ((p '&' r) 'or' ('not' (('not' q) 'or' ('not' r)))) in TAUT by Lm6;
( ('not' (q '&' r)) => (('not' q) 'or' ('not' r)) in TAUT & (('not' (q '&' r)) => (('not' q) 'or' ('not' r))) => (('not' (('not' q) 'or' ('not' r))) => (q '&' r)) in TAUT ) by Th17, LUKASI_1:31;
then ('not' (('not' q) 'or' ('not' r))) => (q '&' r) in TAUT by CQC_THE1:46;
then A5: ((p '&' r) 'or' ('not' (('not' q) 'or' ('not' r)))) => ((p '&' r) 'or' (q '&' r)) in TAUT by Lm7;
r => ('not' ('not' r)) in TAUT by LUKASI_1:27;
then ((p 'or' q) '&' r) => ((p 'or' q) '&' ('not' ('not' r))) in TAUT by Lm5;
then ((p 'or' q) '&' r) => ('not' ((('not' p) 'or' ('not' r)) '&' (('not' q) 'or' ('not' r)))) in TAUT by A3, LUKASI_1:3;
then ((p 'or' q) '&' r) => (('not' (('not' p) 'or' ('not' r))) 'or' ('not' (('not' q) 'or' ('not' r)))) in TAUT by A1, LUKASI_1:3;
then ((p 'or' q) '&' r) => ((p '&' r) 'or' ('not' (('not' q) 'or' ('not' r)))) in TAUT by A4, LUKASI_1:3;
hence ((p 'or' q) '&' r) => ((p '&' r) 'or' (q '&' r)) in TAUT by A5, LUKASI_1:3; :: thesis: verum