let G be Group; :: thesis: for A being Subset of G st ( for g1, g2 being Element of G st g1 in A & g2 in A holds
g1 * g2 in A ) & ( for g being Element of G st g in A holds
g " in A ) holds
A * A = A
let A be Subset of G; :: thesis: ( ( for g1, g2 being Element of G st g1 in A & g2 in A holds
g1 * g2 in A ) & ( for g being Element of G st g in A holds
g " in A ) implies A * A = A )
assume that
A1: for g1, g2 being Element of G st g1 in A & g2 in A holds
g1 * g2 in A and
A2: for g being Element of G st g in A holds
g " in A ; :: thesis: A * A = A
thus A * A c= A :: according to XBOOLE_0:def 10 :: thesis: A c= A * A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A * A or x in A )
assume x in A * A ; :: thesis: x in A
then ex g1, g2 being Element of G st
( x = g1 * g2 & g1 in A & g2 in A ) ;
hence x in A by A1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in A * A )
assume A3: x in A ; :: thesis: x in A * A
then reconsider a = x as Element of G ;
a " in A by A2, A3;
then (a ") * a in A by A1, A3;
then A4: 1_ G in A by GROUP_1:def 5;
(1_ G) * a = a by GROUP_1:def 4;
hence x in A * A by A3, A4; :: thesis: verum