let G be Group; 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; ( ( 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
; A * A = A
thus
A * A c= A
XBOOLE_0:def 10 A c= A * A
let x be object ; TARSKI:def 3 ( not x in A or x in A * A )
assume A3:
x in A
; 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; verum