let A be QC-alphabet ; :: thesis: for p, q, r being Element of CQC-WFF A holds ((p 'or' q) 'or' r) => (p 'or' (q 'or' r)) in TAUT A
let p, q, r be Element of CQC-WFF A; :: thesis: ((p 'or' q) 'or' r) => (p 'or' (q 'or' r)) in TAUT A
( ('not' p) => ((('not' r) => q) => (('not' q) => r)) in TAUT A & (('not' p) => ((('not' r) => q) => (('not' q) => r))) => ((('not' p) => (('not' r) => q)) => (('not' p) => (('not' q) => r))) in TAUT A ) by LUKASI_1:11, LUKASI_1:13, LUKASI_1:31;
then A1: (('not' p) => (('not' r) => q)) => (('not' p) => (('not' q) => r)) in TAUT A by CQC_THE1:46;
( ((p 'or' q) 'or' r) => (r 'or' (p 'or' q)) in TAUT A & (r 'or' (p 'or' q)) => (('not' r) => (p 'or' q)) in TAUT A ) by Th5, Th8;
then ((p 'or' q) 'or' r) => (('not' r) => (p 'or' q)) in TAUT A by LUKASI_1:3;
then A2: ((p 'or' q) 'or' r) => (('not' r) => (('not' p) => q)) in TAUT A by Lm1;
(('not' r) => (('not' p) => q)) => (('not' p) => (('not' r) => q)) in TAUT A by LUKASI_1:8;
then ((p 'or' q) 'or' r) => (('not' p) => (('not' r) => q)) in TAUT A by A2, LUKASI_1:3;
then ((p 'or' q) 'or' r) => (('not' p) => (('not' q) => r)) in TAUT A by A1, LUKASI_1:3;
then ((p 'or' q) 'or' r) => (('not' p) => (q 'or' r)) in TAUT A by Lm1;
hence ((p 'or' q) 'or' r) => (p 'or' (q 'or' r)) in TAUT A by Lm1; :: thesis: verum