let G be non empty addMagma ; 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; ( G is add-associative implies (A + B) + C = A + (B + C) )
assume A1:
G is add-associative
; (A + B) + C = A + (B + C)
thus
(A + B) + C c= A + (B + C)
XBOOLE_0:def 10 A + (B + C) c= (A + B) + C
let x be object ; TARSKI:def 3 ( not x in A + (B + C) or x in (A + B) + C )
assume
x in A + (B + C)
; 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; verum