let G be non empty addMagma ; :: thesis: for A, B being Subset of G st ( for a, b being Element of G st a in A & b in B holds
a + b = b + a ) holds
A + B = B + A
let A, B be Subset of G; :: thesis: ( ( for a, b being Element of G st a in A & b in B holds
a + b = b + a ) implies A + B = B + A )
assume A1: for a, b being Element of G st a in A & b in B holds
a + b = b + a ; :: thesis: A + B = B + A
thus A + B c= B + A :: according to XBOOLE_0:def 10 :: thesis: B + A c= A + B

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A + B or x in B + A )
assume x in A + B ; :: thesis: x in B + A
then consider a, b being Element of G such that
A2: x = a + b and
A3: ( a in A & b in B ) ;
x = b + a by A1, A2, A3;
hence x in B + A by A3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B + A or x in A + B )
assume x in B + A ; :: thesis: x in A + B
then consider b, a being Element of G such that
A4: x = b + a and
A5: ( b in B & a in A ) ;
x = a + b by A1, A4, A5;
hence x in A + B by A5; :: thesis: verum