let p, q, r be Element of CQC-WFF ; :: thesis: ((p 'or' q) '&' r) => ((p '&' r) 'or' (q '&' r)) in TAUT
((('not' p) 'or' ('not' r)) '&' (('not' q) 'or' ('not' r))) => ((('not' p) '&' ('not' q)) 'or' ('not' r)) in TAUT by Th40;
then A1: ('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 A1, LUKASI_1:3;
then A2: ((p 'or' q) '&' ('not' ('not' r))) => ('not' ((('not' p) 'or' ('not' r)) '&' (('not' q) 'or' ('not' r)))) in TAUT by QC_LANG2:def 3;
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 A3: ((p 'or' q) '&' r) => ('not' ((('not' p) 'or' ('not' r)) '&' (('not' q) 'or' ('not' r)))) in TAUT by A2, LUKASI_1:3;
('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;
then A4: ((p 'or' q) '&' r) => (('not' (('not' p) 'or' ('not' r))) 'or' ('not' (('not' q) 'or' ('not' r)))) in TAUT by A3, LUKASI_1:3;
A5: ('not' (p '&' r)) => (('not' p) 'or' ('not' r)) in TAUT by Th17;
(('not' (p '&' r)) => (('not' p) 'or' ('not' r))) => (('not' (('not' p) 'or' ('not' r))) => (p '&' r)) in TAUT by LUKASI_1:31;
then ('not' (('not' p) 'or' ('not' r))) => (p '&' r) in TAUT by A5, CQC_THE1:82;
then (('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;
then A6: ((p 'or' q) '&' r) => ((p '&' r) 'or' ('not' (('not' q) 'or' ('not' r)))) in TAUT by A4, LUKASI_1:3;
A7: ('not' (q '&' r)) => (('not' q) 'or' ('not' r)) in TAUT by Th17;
(('not' (q '&' r)) => (('not' q) 'or' ('not' r))) => (('not' (('not' q) 'or' ('not' r))) => (q '&' r)) in TAUT by LUKASI_1:31;
then ('not' (('not' q) 'or' ('not' r))) => (q '&' r) in TAUT by A7, CQC_THE1:82;
then ((p '&' r) 'or' ('not' (('not' q) 'or' ('not' r)))) => ((p '&' r) 'or' (q '&' r)) in TAUT by Lm7;
hence ((p 'or' q) '&' r) => ((p '&' r) 'or' (q '&' r)) in TAUT by A6, LUKASI_1:3; :: thesis: verum