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