set M = { a where a is Element of R : a * J c= I } ;
for x being object st x in { a where a is Element of R : a * J c= I } holds
x in the carrier of R

proof

let x be object ; :: thesis: ( x in { a where a is Element of R : a * J c= I } implies x in the carrier of R )
assume x in { a where a is Element of R : a * J c= I } ; :: thesis: x in the carrier of R
then ex a being Element of R st
( x = a & a * J c= I ) ;
hence x in the carrier of R ; :: thesis: verum

end;

hence { a where a is Element of R : a * J c= I } is Subset of R by TARSKI:def 3; :: thesis: verum