let p, q, r be Element of CQC-WFF ; :: thesis: ((p 'or' q) '&' (p 'or' r)) => (p 'or' (q '&' r)) in TAUT
(('not' p) => q) => ((('not' p) => r) => (('not' p) => (q '&' r))) in TAUT by Th33;
then (p 'or' q) => ((('not' p) => r) => (('not' p) => (q '&' r))) in TAUT by Lm1;
then (p 'or' q) => ((p 'or' r) => (('not' p) => (q '&' r))) in TAUT by Lm1;
then A1: (p 'or' q) => ((p 'or' r) => (p 'or' (q '&' r))) in TAUT by Lm1;
((p 'or' q) => ((p 'or' r) => (p 'or' (q '&' r)))) => (((p 'or' q) '&' (p 'or' r)) => (p 'or' (q '&' r))) in TAUT by Th32;
hence ((p 'or' q) '&' (p 'or' r)) => (p 'or' (q '&' r)) in TAUT by A1, CQC_THE1:46; :: thesis: verum