let IT, X be Subset of REAL ; :: thesis: ( IT = { (- r3) where r3 is Real : r3 in X } implies X = { (- r3) where r3 is Real : r3 in IT } )
assume A1: IT = { (- r3) where r3 is Real : r3 in X } ; :: thesis: X = { (- r3) where r3 is Real : r3 in IT }
thus X c= { (- r3) where r3 is Real : r3 in IT } :: according to XBOOLE_0:def 10 :: thesis: { (- r3) where r3 is Real : r3 in IT } c= X

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in X or e in { (- r3) where r3 is Real : r3 in IT } )
assume A2: e in X ; :: thesis: e in { (- r3) where r3 is Real : r3 in IT }
then reconsider r0 = e as Element of REAL ;
A3: e = - (- r0) ;
- r0 in IT by A1, A2;
hence e in { (- r3) where r3 is Real : r3 in IT } by A3; :: thesis: verum

end;

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { (- r3) where r3 is Real : r3 in IT } or e in X )
assume e in { (- r3) where r3 is Real : r3 in IT } ; :: thesis: e in X
then consider r0 being Element of REAL such that
A4: - r0 = e and
A5: r0 in IT ;
ex r1 being Element of REAL st
( - r1 = r0 & r1 in X ) by A1, A5;
hence e in X by A4; :: thesis: verum