let V be non empty add-associative addLoopStr ; :: thesis: for A being Subset of V
for v, w being Element of V holds (v + w) + A = v + (w + A)
let A be Subset of V; :: thesis: for v, w being Element of V holds (v + w) + A = v + (w + A)
let v, w be Element of V; :: thesis: (v + w) + A = v + (w + A)
set vw = v + w;
thus (v + w) + A c= v + (w + A) :: according to XBOOLE_0:def 10 :: thesis: v + (w + A) c= (v + w) + A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (v + w) + A or x in v + (w + A) )
assume x in (v + w) + A ; :: thesis: x in v + (w + A)
then consider s being Element of V such that
A1: ( x = (v + w) + s & s in A ) ;
( w + s in w + A & x = v + (w + s) ) by A1, RLVECT_1:def 3;
hence x in v + (w + A) ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in v + (w + A) or x in (v + w) + A )
assume x in v + (w + A) ; :: thesis: x in (v + w) + A
then consider s being Element of V such that
A2: x = v + s and
A3: s in w + A ;
consider r being Element of V such that
A4: s = w + r and
A5: r in A by A3;
x = (v + w) + r by A2, A4, RLVECT_1:def 3;
hence x in (v + w) + A by A5; :: thesis: verum