let A be QC-alphabet ; for p, q, r being Element of CQC-WFF A holds (p '&' (q 'or' r)) => ((p '&' q) 'or' (p '&' r)) in TAUT A
let p, q, r be Element of CQC-WFF A; (p '&' (q 'or' r)) => ((p '&' q) 'or' (p '&' r)) in TAUT A
A1:
('not' ((p '&' q) 'or' (p '&' r))) => (('not' (p '&' q)) '&' ('not' (p '&' r))) in TAUT A
by Th6;
( ('not' (p => ('not' q))) => (p '&' q) in TAUT A & (('not' (p => ('not' q))) => (p '&' q)) => (('not' (p '&' q)) => (p => ('not' q))) in TAUT A )
by Th16, LUKASI_1:31;
then A2:
('not' (p '&' q)) => (p => ('not' q)) in TAUT A
by CQC_THE1:46;
( ('not' (p => ('not' r))) => (p '&' r) in TAUT A & (('not' (p => ('not' r))) => (p '&' r)) => (('not' (p '&' r)) => (p => ('not' r))) in TAUT A )
by Th16, LUKASI_1:31;
then A3:
('not' (p '&' r)) => (p => ('not' r)) in TAUT A
by CQC_THE1:46;
( (p => ('not' q)) => ((p => ('not' r)) => (p => (('not' q) '&' ('not' r)))) in TAUT A & p => (('not' q) '&' ('not' r)) = 'not' (p '&' ('not' (('not' q) '&' ('not' r)))) )
by Th33, QC_LANG2:def 2;
then
(p => ('not' q)) => ((p => ('not' r)) => ('not' (p '&' (q 'or' r)))) in TAUT A
by QC_LANG2:def 3;
then
('not' (p '&' q)) => ((p => ('not' r)) => ('not' (p '&' (q 'or' r)))) in TAUT A
by A2, LUKASI_1:3;
then
(p => ('not' r)) => (('not' (p '&' q)) => ('not' (p '&' (q 'or' r)))) in TAUT A
by LUKASI_1:15;
then
('not' (p '&' r)) => (('not' (p '&' q)) => ('not' (p '&' (q 'or' r)))) in TAUT A
by A3, LUKASI_1:3;
then A4:
('not' (p '&' q)) => (('not' (p '&' r)) => ('not' (p '&' (q 'or' r)))) in TAUT A
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 A
by Th32;
then
(('not' (p '&' q)) '&' ('not' (p '&' r))) => ('not' (p '&' (q 'or' r))) in TAUT A
by A4, CQC_THE1:46;
then
('not' ((p '&' q) 'or' (p '&' r))) => ('not' (p '&' (q 'or' r))) in TAUT A
by A1, LUKASI_1:3;
hence
(p '&' (q 'or' r)) => ((p '&' q) 'or' (p '&' r)) in TAUT A
by LUKASI_1:35; verum