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

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

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 { (g ") where g is Element of G : g in R } or a in B )
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;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

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