set Y = { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes n) : verum } ;
{ (1 / (Product (Sgm X))) where X is Subset of (SetPrimes n) : verum } c= REAL

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes n) : verum } or x in REAL )
assume x in { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes n) : verum } ; :: thesis: x in REAL
then consider X being Subset of (SetPrimes n) such that
A1: x = 1 / (Product (Sgm X)) ;
thus x in REAL by A1, XREAL_0:def 1; :: thesis: verum

end;

hence { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes n) : verum } is Subset of REAL ; :: thesis: verum