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