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

hereby :: thesis: ( a " in A implies a in A " )

assume a in A " ; :: thesis: a " in A
then consider g being Element of G such that
A2: ( a = g " & g in A ) by A1;
thus a " in A by A2, GROUP_1:19; :: thesis: verum

end;

assume A3: a " in A ; :: thesis: a in A "
(a " ) " = a by GROUP_1:19;
hence a in A " by A1, A3; :: thesis: verum