set M = { a where a is Element of R : a * J c= I } ;
{ a where a is Element of R : a * J c= I } is non empty Subset of R

proof

A1: (0. R) * J = {(0. R)} by Th70;
( 0. R in I & 0. R in J ) by Th2;
then for u being set st u in {(0. R)} holds
u in I by TARSKI:def 1;
then {(0. R)} c= I by TARSKI:def 3;
then A2: 0. R in { a where a is Element of R : a * J c= I } by A1;
for x being set 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 set ; :: 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 consider a being Element of R such that
A3: ( x = a & a * J c= I ) ;
thus x in the carrier of R by A3; :: thesis: verum

end;

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

end;

hence not I % J is empty ; :: thesis: verum