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

proof

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

end;

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { (1 / r3) where r3 is Real : r3 in Y } or e in X )
assume e in { (1 / r3) where r3 is Real : r3 in Y } ; :: thesis: e in X
then consider r3 being Real such that
A4: e = 1 / r3 and
A5: r3 in Y ;
ex r1 being Real st
( r3 = 1 / r1 & r1 in X ) by A1, A5;
hence e in X by A4; :: thesis: verum