let R be non empty add-associative addLoopStr ; :: thesis: for I, J, K being Subset of R holds I + (J + K) = (I + J) + K
let I, J, K be Subset of R; :: thesis: I + (J + K) = (I + J) + K

A1: now

let u be set ; :: thesis: ( u in (I + J) + K implies u in I + (J + K) )
assume u in (I + J) + K ; :: thesis: u in I + (J + K)
then consider a, b being Element of R such that
A2: u = a + b and
A3: a in I + J and
A4: b in K ;
consider c, d being Element of R such that
A5: a = c + d and
A6: c in I and
A7: d in J by A3;
d + b in { (a' + b') where a', b' is Element of R : ( a' in J & b' in K ) } by A4, A7;
then c + (d + b) in { (a' + b') where a', b' is Element of R : ( a' in I & b' in J + K ) } by A6;
hence u in I + (J + K) by A2, A5, RLVECT_1:def 6; :: thesis: verum

end;

now

let u be set ; :: thesis: ( u in I + (J + K) implies u in (I + J) + K )
assume u in I + (J + K) ; :: thesis: u in (I + J) + K
then consider a, b being Element of R such that
A8: u = a + b and
A9: a in I and
A10: b in J + K ;
consider c, d being Element of R such that
A11: b = c + d and
A12: c in J and
A13: d in K by A10;
a + c in { (a' + b') where a', b' is Element of R : ( a' in I & b' in J ) } by A9, A12;
then (a + c) + d in { (a' + b') where a', b' is Element of R : ( a' in I + J & b' in K ) } by A13;
hence u in (I + J) + K by A8, A11, RLVECT_1:def 6; :: thesis: verum

end;

hence I + (J + K) = (I + J) + K by A1, TARSKI:2; :: thesis: verum