set M = { a where a is Element of R : a * J c= I } ;
0. R in I by Th2;
then for u being object st u in {(0. R)} holds
u in I by TARSKI:def 1;
then A1: {(0. R)} c= I ;
(0. R) * J = {(0. R)} by Th70;
then 0. R in { a where a is Element of R : a * J c= I } by A1;
hence not I % J is empty ; :: thesis: verum