set M = { a where a is Element of R : a * J c= I } ;
{ a where a is Element of R : a * J c= I } = I % J ;
then reconsider M = { a where a is Element of R : a * J c= I } as non empty Subset of R ;
for x, y being Element of R st x in M & y in M holds
x + y in M

proof

let x, y be Element of R; :: thesis: ( x in M & y in M implies x + y in M )
assume that
A1: x in M and
A2: y in M ; :: thesis: x + y in M
consider b being Element of R such that
A3: y = b and
A4: b * J c= I by A2;
consider a being Element of R such that
A5: x = a and
A6: a * J c= I by A1;

now :: thesis: for u being object st u in (a + b) * J holds
u in I

let u be object ; :: thesis: ( u in (a + b) * J implies u in I )
assume u in (a + b) * J ; :: thesis: u in I
then consider c being Element of R such that
A7: u = (a + b) * c and
A8: c in J ;
A9: b * c in { (b * i) where i is Element of R : i in J } by A8;
( u = (a * c) + (b * c) & a * c in a * J ) by A7, A8, VECTSP_1:def 3;
hence u in I by A6, A4, A9, Def1; :: thesis: verum

end;

then (a + b) * J c= I ;
hence x + y in M by A5, A3; :: thesis: verum

end;

hence I % J is add-closed ; :: thesis: verum