let A, B be Subset of G; :: 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 ex g, h being Element of G st
( x = g + h & g in A & h in B ) ;
hence x in B + A ; :: 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 ex g, h being Element of G st
( x = g + h & g in B & h in A ) ;
hence x in A + B ; :: thesis: verum