let G be non empty addMagma ; :: thesis: for A, B being Subset of G st G is Abelian addGroup holds
A + B = B + A
let A, B be Subset of G; :: thesis: ( G is Abelian addGroup implies A + B = B + A )
assume A1: G is Abelian addGroup ; :: 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 g, h being Element of G such that
A2: x = g + h and
A3: ( g in A & h in B ) ;
x = h + g by A1, A2, Lm2;
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 g, h being Element of G such that
A4: x = g + h and
A5: ( g in B & h in A ) ;
x = h + g by A1, A4, Lm2;
hence x in A + B by A5; :: thesis: verum