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
A1: ( x = ab + c & ab in A + B & c in C ) ;
consider a, b being Element of E such that
A2: ( ab = a + b & a in A & b in B ) by A1;
A3: x = a + (b + c) by A1, A2, RLVECT_1:def 3;
b + c in B + C by A1, A2;
hence x in A + (B + C) by A2, A3; :: 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
A4: ( x = a + bc & a in A & bc in B + C ) ;
consider b, c being Element of E such that
A5: ( bc = b + c & b in B & c in C ) by A4;
A6: x = (a + b) + c by A4, A5, RLVECT_1:def 3;
a + b in A + B by A4, A5;
hence x in (A + B) + C by A5, A6; :: thesis: verum

end;

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