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 & a in I & b in J + K ) ;
consider c, d being Element of R such that
A3: ( b = c + d & c in J & d in K ) by A2;
a + c in { (a' + b') where a', b' is Element of R : ( a' in I & b' in J ) } by A2, A3;
then (a + c) + d in { (a' + b') where a', b' is Element of R : ( a' in I + J & b' in K ) } by A3;
hence u in (I + J) + K by A2, A3, 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
A4: ( u = a + b & a in I + J & b in K ) ;
consider c, d being Element of R such that
A5: ( a = c + d & c in I & d in J ) by A4;
d + b in { (a' + b') where a', b' is Element of R : ( a' in J & b' in K ) } by A4, A5;
then c + (d + b) in { (a' + b') where a', b' is Element of R : ( a' in I & b' in J + K ) } by A5;
hence u in I + (J + K) by A4, A5, RLVECT_1:def 6; :: thesis: verum

end;

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