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