let G be Group; :: thesis: ( G is commutative Group iff for A being Subset of G
for g being Element of G holds A |^ g = A )
thus ( G is commutative Group implies for A being Subset of G
for g being Element of G holds A |^ g = A ) by Th55; :: thesis: ( ( for A being Subset of G
for g being Element of G holds A |^ g = A ) implies G is commutative Group )
assume A1: for A being Subset of G
for g being Element of G holds A |^ g = 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 A1
.= {(a |^ b)} by Th37 ;
hence a = a |^ b by ZFMISC_1:3; :: thesis: verum
end;
hence G is commutative Group by Th30; :: thesis: verum