let G be non empty multMagma ; :: thesis: for A, B being Subset of G st G is commutative Group holds
A * B = B * A
let A, B be Subset of G; :: thesis: ( G is commutative Group implies A * B = B * A )
assume A1: G is commutative Group ; :: 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