set Y = { (1 / r3) where r3 is Real : r3 in X } ;
{ (1 / r3) where r3 is Real : r3 in X } c= REAL

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { (1 / r3) where r3 is Real : r3 in X } or e in REAL )
assume e in { (1 / r3) where r3 is Real : r3 in X } ; :: thesis: e in REAL
then ex r3 being Real st
( e = 1 / r3 & r3 in X ) ;
hence e in REAL by XREAL_0:def 1; :: thesis: verum

end;

hence { (1 / r3) where r3 is Real : r3 in X } is Subset of REAL ; :: thesis: verum