let p, q, r be Element of CQC-WFF ; :: thesis: (p '&' (q 'or' r)) => ((p '&' q) 'or' (p '&' r)) in TAUT
A1: (p => ('not' q)) => ((p => ('not' r)) => (p => (('not' q) '&' ('not' r)))) in TAUT by Th33;
p => (('not' q) '&' ('not' r)) = 'not' (p '&' ('not' (('not' q) '&' ('not' r)))) by QC_LANG2:def 2;
then A2: (p => ('not' q)) => ((p => ('not' r)) => ('not' (p '&' (q 'or' r)))) in TAUT by A1, QC_LANG2:def 3;
A3: ('not' (p => ('not' q))) => (p '&' q) in TAUT by Th16;
(('not' (p => ('not' q))) => (p '&' q)) => (('not' (p '&' q)) => (p => ('not' q))) in TAUT by LUKASI_1:31;
then ('not' (p '&' q)) => (p => ('not' q)) in TAUT by A3, CQC_THE1:82;
then ('not' (p '&' q)) => ((p => ('not' r)) => ('not' (p '&' (q 'or' r)))) in TAUT by A2, LUKASI_1:3;
then A4: (p => ('not' r)) => (('not' (p '&' q)) => ('not' (p '&' (q 'or' r)))) in TAUT by LUKASI_1:15;
A5: ('not' (p => ('not' r))) => (p '&' r) in TAUT by Th16;
(('not' (p => ('not' r))) => (p '&' r)) => (('not' (p '&' r)) => (p => ('not' r))) in TAUT by LUKASI_1:31;
then ('not' (p '&' r)) => (p => ('not' r)) in TAUT by A5, CQC_THE1:82;
then ('not' (p '&' r)) => (('not' (p '&' q)) => ('not' (p '&' (q 'or' r)))) in TAUT by A4, LUKASI_1:3;
then A6: ('not' (p '&' q)) => (('not' (p '&' r)) => ('not' (p '&' (q 'or' r)))) in TAUT by LUKASI_1:15;
(('not' (p '&' q)) => (('not' (p '&' r)) => ('not' (p '&' (q 'or' r))))) => ((('not' (p '&' q)) '&' ('not' (p '&' r))) => ('not' (p '&' (q 'or' r)))) in TAUT by Th32;
then A7: (('not' (p '&' q)) '&' ('not' (p '&' r))) => ('not' (p '&' (q 'or' r))) in TAUT by A6, CQC_THE1:82;
('not' ((p '&' q) 'or' (p '&' r))) => (('not' (p '&' q)) '&' ('not' (p '&' r))) in TAUT by Th6;
then ('not' ((p '&' q) 'or' (p '&' r))) => ('not' (p '&' (q 'or' r))) in TAUT by A7, LUKASI_1:3;
hence (p '&' (q 'or' r)) => ((p '&' q) 'or' (p '&' r)) in TAUT by LUKASI_1:35; :: thesis: verum