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