let G be Group; :: thesis: ( G is commutative Group iff for A, B being Subset of G st B <> {} holds
A |^ B = A )
thus ( G is commutative Group implies for A, B being Subset of G st B <> {} holds
A |^ B = A ) :: thesis: ( ( for A, B being Subset of G st B <> {} holds
A |^ B = A ) implies G is commutative Group )

proof

assume A1: G is commutative Group ; :: thesis: for A, B being Subset of G st B <> {} holds
A |^ B = A
let A, B be Subset of G; :: thesis: ( B <> {} implies A |^ B = A )
set y = the Element of B;
assume A2: B <> {} ; :: thesis: A |^ B = A
then reconsider y = the Element of B as Element of G by TARSKI:def 3;
thus A |^ B c= A :: according to XBOOLE_0:def 10 :: thesis: A c= A |^ B

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A |^ B or x in A )
assume x in A |^ B ; :: thesis: x in A
then ex a, b being Element of G st
( x = a |^ b & a in A & b in B ) ;
hence x in A by A1, Th29; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in A |^ B )
assume A3: x in A ; :: thesis: x in A |^ B
then reconsider a = x as Element of G ;
a |^ y = x by A1, Th29;
hence x in A |^ B by A2, A3; :: thesis: verum

end;

assume A4: for A, B being Subset of G st B <> {} holds
A |^ B = A ; :: thesis: G is commutative Group

now :: thesis: for a, b being Element of G holds a = a |^ b

let a, b be Element of G; :: thesis: a = a |^ b
{a} = {a} |^ {b} by A4
.= {(a |^ b)} by Th37 ;
hence a = a |^ b by ZFMISC_1:3; :: thesis: verum

end;

hence G is commutative Group by Th30; :: thesis: verum