let A be QC-alphabet ; :: thesis: for p, q, r being Element of CQC-WFF A holds ((p 'or' q) '&' r) => ((p '&' r) 'or' (q '&' r)) in TAUT A
let p, q, r be Element of CQC-WFF A; :: thesis: ((p 'or' q) '&' r) => ((p '&' r) 'or' (q '&' r)) in TAUT A
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 A by Th17;
((('not' p) 'or' ('not' r)) '&' (('not' q) 'or' ('not' r))) => ((('not' p) '&' ('not' q)) 'or' ('not' r)) in TAUT A 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 A by LUKASI_1:34;
(('not' (('not' p) '&' ('not' q))) '&' ('not' ('not' r))) => ('not' ((('not' p) '&' ('not' q)) 'or' ('not' r))) in TAUT A by Th7;
then (('not' (('not' p) '&' ('not' q))) '&' ('not' ('not' r))) => ('not' ((('not' p) 'or' ('not' r)) '&' (('not' q) 'or' ('not' r)))) in TAUT A 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 A by QC_LANG2:def 3;
( ('not' (p '&' r)) => (('not' p) 'or' ('not' r)) in TAUT A & (('not' (p '&' r)) => (('not' p) 'or' ('not' r))) => (('not' (('not' p) 'or' ('not' r))) => (p '&' r)) in TAUT A ) by Th17, LUKASI_1:31;
then ('not' (('not' p) 'or' ('not' r))) => (p '&' r) in TAUT A 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 A by Lm6;
( ('not' (q '&' r)) => (('not' q) 'or' ('not' r)) in TAUT A & (('not' (q '&' r)) => (('not' q) 'or' ('not' r))) => (('not' (('not' q) 'or' ('not' r))) => (q '&' r)) in TAUT A ) by Th17, LUKASI_1:31;
then ('not' (('not' q) 'or' ('not' r))) => (q '&' r) in TAUT A by CQC_THE1:46;
then A5: ((p '&' r) 'or' ('not' (('not' q) 'or' ('not' r)))) => ((p '&' r) 'or' (q '&' r)) in TAUT A by Lm7;
r => ('not' ('not' r)) in TAUT A by LUKASI_1:27;
then ((p 'or' q) '&' r) => ((p 'or' q) '&' ('not' ('not' r))) in TAUT A by Lm5;
then ((p 'or' q) '&' r) => ('not' ((('not' p) 'or' ('not' r)) '&' (('not' q) 'or' ('not' r)))) in TAUT A 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 A by A1, LUKASI_1:3;
then ((p 'or' q) '&' r) => ((p '&' r) 'or' ('not' (('not' q) 'or' ('not' r)))) in TAUT A by A4, LUKASI_1:3;
hence ((p 'or' q) '&' r) => ((p '&' r) 'or' (q '&' r)) in TAUT A by A5, LUKASI_1:3; :: thesis: verum