let G be addGroup; :: thesis: ( G is Abelian addGroup iff for A, B being Subset of G st B <> {} holds
A * B = A )
thus ( G is Abelian addGroup 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 Abelian addGroup )

proof

assume A1: G is Abelian addGroup ; :: 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 Abelian addGroup

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 ThB37 ;
hence a = a * b by ZFMISC_1:3; :: thesis: verum

end;

hence G is Abelian addGroup by ThB30; :: thesis: verum