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

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

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 B * A or x in A * B )
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;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

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