let R, B be Subset of G; :: thesis: ( R = { (- g) where g is Element of G : g in B } implies B = { (- g) where g is Element of G : g in R } )
assume A1: R = { (- g) where g is Element of G : g in B } ; :: thesis: B = { (- g) where g is Element of G : g in R }
thus B c= { (- g) where g is Element of G : g in R } :: according to XBOOLE_0:def 10 :: thesis: { (- g) where g is Element of G : g in R } c= B

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in B or a in { (- g) where g is Element of G : g in R } )
assume A2: a in B ; :: thesis: a in { (- g) where g is Element of G : g in R }
then reconsider a = a as Element of G ;
( - (- a) = a & - a in R ) by A1, A2;
hence a in { (- g) where g is Element of G : g in R } ; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (- g) where g is Element of G : g in R } or a in B )
assume a in { (- g) where g is Element of G : g in R } ; :: thesis: a in B
then consider g being Element of G such that
A3: a = - g and
A4: g in R ;
ex h being Element of G st
( g = - h & h in B ) by A1, A4;
hence a in B by A3; :: thesis: verum