set M = { a where a is Element of R : ex n being Element of NAT st a |^ n in I } ;
{ a where a is Element of R : ex n being Element of NAT st a |^ n in I } is Subset of R

proof

for x being set st x in { a where a is Element of R : ex n being Element of NAT st a |^ n in I } holds
x in the carrier of R

proof

let x be set ; :: thesis: ( x in { a where a is Element of R : ex n being Element of NAT st a |^ n in I } implies x in the carrier of R )
assume x in { a where a is Element of R : ex n being Element of NAT st a |^ n in I } ; :: thesis: x in the carrier of R
then consider a being Element of R such that
A1: ( a = x & ex n being Element of NAT st a |^ n in I ) ;
thus x in the carrier of R by A1; :: thesis: verum

end;

hence { a where a is Element of R : ex n being Element of NAT st a |^ n in I } is Subset of R by TARSKI:def 3; :: thesis: verum

end;

hence { a where a is Element of R : ex n being Element of NAT st a |^ n in I } is Subset of R ; :: thesis: verum