let E be non empty add-associative addLoopStr ; :: thesis: for A, B, C being Subset of E holds (A + B) + C = A + (B + C)
let A, B, C be Subset of E; :: thesis: (A + B) + C = A + (B + C)
for x being Element of E holds
( x in (A + B) + C iff x in A + (B + C) )

proof

let x be Element of E; :: thesis: ( x in (A + B) + C iff x in A + (B + C) )

hereby :: thesis: ( x in A + (B + C) implies x in (A + B) + C )

assume x in (A + B) + C ; :: thesis: x in A + (B + C)
then consider ab, c being Element of E such that
P1: ( x = ab + c & ab in A + B & c in C ) ;
consider a, b being Element of E such that
P2: ( ab = a + b & a in A & b in B ) by P1;
P3: x = a + (b + c) by P1, P2, RLVECT_1:def 3;
b + c in B + C by P1, P2;
hence x in A + (B + C) by P2, P3; :: thesis: verum

end;

assume x in A + (B + C) ; :: thesis: x in (A + B) + C
then consider a, bc being Element of E such that
P1: ( x = a + bc & a in A & bc in B + C ) ;
consider b, c being Element of E such that
P2: ( bc = b + c & b in B & c in C ) by P1;
P3: x = (a + b) + c by P1, P2, RLVECT_1:def 3;
a + b in A + B by P1, P2;
hence x in (A + B) + C by P2, P3; :: thesis: verum

end;

hence (A + B) + C = A + (B + C) by SUBSET_1:3; :: thesis: verum