let AFV be WeakAffVect; for o being Element of
for a, b, c being Element of holds (a + b) + c = a + (b + c)
let o be Element of ; for a, b, c being Element of holds (a + b) + c = a + (b + c)
let a, b, c be Element of ; (a + b) + c = a + (b + c)
reconsider a' = a, b' = b, c' = c as Element of ;
set p = b + c;
set q = a + b;
reconsider p' = b + c, q' = a + b as Element of ;
reconsider x' = a + (b + c), y' = (a + b) + c as Element of ;
consider x'' being Element of such that
A1:
x',p' // c',x''
by Def1;
x' = Padd o,a',p'
by Def7;
then
o,a' // p',x'
by Def5;
then A2:
a',o // x',p'
by Th8;
c',x'' // x',p'
by A1, Th4;
then A3:
a',o // c',x''
by A2, Def1;
q' = Padd o,a',b'
by Def7;
then
o,a' // b',q'
by Def5;
then
o,b' // a',q'
by Def1;
then A4:
a',q' // o,b'
by Th4;
p' = Padd o,b',c'
by Def7;
then
o,b' // c',p'
by Def5;
then
c',p' // o,b'
by Th4;
then
a',q' // c',p'
by A4, Def1;
then A5:
q',o // p',x''
by A3, Def1;
x',c' // p',x''
by A1, Def1;
then
q',o // x',c'
by A5, Def1;
then
o,q' // c',x'
by Th8;
then A6:
c',x' // o,q'
by Th4;
y' = Padd o,q',c'
by Def7;
then
o,q' // c',y'
by Def5;
then
c',y' // o,q'
by Th4;
then
c',y' // c',x'
by A6, Def1;
hence
(a + b) + c = a + (b + c)
by Th5; verum