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
A1: (('not' p) => (('not' r) => q)) => (('not' r) => (('not' p) => q)) in TAUT A by LUKASI_1:8;
( ('not' p) => ((('not' q) => r) => (('not' r) => q)) in TAUT A & (('not' p) => ((('not' q) => r) => (('not' r) => q))) => ((('not' p) => (('not' q) => r)) => (('not' p) => (('not' r) => q))) in TAUT A ) by LUKASI_1:11, LUKASI_1:13, LUKASI_1:31;
then A2: (('not' p) => (('not' q) => r)) => (('not' p) => (('not' r) => q)) in TAUT A by CQC_THE1:46;
(p 'or' (q 'or' r)) => (('not' p) => (q 'or' r)) in TAUT A by Th5;
then (p 'or' (q 'or' r)) => (('not' p) => (('not' q) => r)) in TAUT A by Lm1;
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' r) => (('not' p) => q)) in TAUT A by A1, LUKASI_1:3;
then A3: (p 'or' (q 'or' r)) => (r 'or' (('not' p) => q)) in TAUT A by Lm1;
(r 'or' (('not' p) => q)) => ((('not' p) => q) 'or' r) in TAUT A by Th8;
then (p 'or' (q 'or' r)) => ((('not' p) => q) 'or' r) in TAUT A by A3, LUKASI_1:3;
hence (p 'or' (q 'or' r)) => ((p 'or' q) 'or' r) in TAUT A by Lm1; :: thesis: verum