let G be non empty addMagma ; :: thesis: for A, B, C being Subset of G st G is add-associative holds
(A + B) + C = A + (B + C)
let A, B, C be Subset of G; :: thesis: ( G is add-associative implies (A + B) + C = A + (B + C) )
assume A1: G is add-associative ; :: thesis: (A + B) + C = A + (B + C)
thus (A + B) + C c= A + (B + C) :: according to XBOOLE_0:def 10 :: thesis: A + (B + C) c= (A + B) + C

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (A + B) + C or x in A + (B + C) )
assume x in (A + B) + C ; :: thesis: x in A + (B + C)
then consider g, h being Element of G such that
A2: x = g + h and
A3: g in A + B and
A4: h in C ;
consider g1, g2 being Element of G such that
A5: g = g1 + g2 and
A6: g1 in A and
A7: g2 in B by A3;
( x = g1 + (g2 + h) & g2 + h in B + C ) by A1, A2, A4, A5, A7;
hence x in A + (B + C) by A6; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A + (B + C) or x in (A + B) + C )
assume x in A + (B + C) ; :: thesis: x in (A + B) + C
then consider g, h being Element of G such that
A8: x = g + h and
A9: g in A and
A10: h in B + C ;
consider g1, g2 being Element of G such that
A11: h = g1 + g2 and
A12: g1 in B and
A13: g2 in C by A10;
A14: g + g1 in A + B by A9, A12;
x = (g + g1) + g2 by A1, A8, A11;
hence x in (A + B) + C by A13, A14; :: thesis: verum