let G be Group; :: thesis: for A being Subset of G st ( for g being Element of G st g in A holds
g " in A ) holds
A " = A
let A be Subset of G; :: thesis: ( ( for g being Element of G st g in A holds
g " in A ) implies A " = A )
assume A1: for g being Element of G st g in A holds
g " in A ; :: thesis: A " = A
thus A " c= A :: according to XBOOLE_0:def 10 :: thesis: A c= A "

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A " or x in A )
assume x in A " ; :: thesis: x in A
then ex g being Element of G st
( x = g " & g 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 " )
assume A2: x in A ; :: thesis: x in A "
then reconsider a = x as Element of G ;
A3: x = (a ") " ;
a " in A by A1, A2;
hence x in A " by A3; :: thesis: verum