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