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 "

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

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 " )
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;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

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