let A be QC-alphabet ; 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; ((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; verum