let G be Group; :: thesis: for A being Subset of G holds (A " ) " = A
let A be Subset of G; :: thesis: (A " ) " = A
A1: (A " ) " = { (g " ) where g is Element of G : g in A " } by GROUP_2:def 1;
A2: A " = { (g " ) where g is Element of G : g in A } by GROUP_2:def 1;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: A c= (A " ) "

let x be set ; :: thesis: ( x in (A " ) " implies x in A )
assume x in (A " ) " ; :: thesis: x in A
then consider g being Element of G such that
A3: ( x = g " & g in A " ) by A1;
consider h being Element of G such that
A4: ( g = h " & h in A ) by A2, A3;
thus x in A by A3, A4, GROUP_1:19; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in (A " ) " )
assume A5: x in A ; :: thesis: x in (A " ) "
then reconsider g = x as Element of G ;
g " in A " by A2, A5;
then (g " ) " in (A " ) " by A1;
hence x in (A " ) " by GROUP_1:19; :: thesis: verum