set M = { (a + b) where a, b is Element of R : ( a in I & b in J ) } ;
for x, y being Element of R st x in { (a + b) where a, b is Element of R : ( a in I & b in J ) } & y in { (a + b) where a, b is Element of R : ( a in I & b in J ) } holds
x + y in { (a + b) where a, b is Element of R : ( a in I & b in J ) }

proof

let x, y be Element of R; :: thesis: ( x in { (a + b) where a, b is Element of R : ( a in I & b in J ) } & y in { (a + b) where a, b is Element of R : ( a in I & b in J ) } implies x + y in { (a + b) where a, b is Element of R : ( a in I & b in J ) } )
assume A1: ( x in { (a + b) where a, b is Element of R : ( a in I & b in J ) } & y in { (a + b) where a, b is Element of R : ( a in I & b in J ) } ) ; :: thesis: x + y in { (a + b) where a, b is Element of R : ( a in I & b in J ) }
then consider a', b' being Element of R such that
A2: ( x = a' + b' & a' in I & b' in J ) ;
consider c, d being Element of R such that
A3: ( y = c + d & c in I & d in J ) by A1;
A4: ( a' + c in I & b' + d in J ) by A2, A3, Def1;
(a' + c) + (b' + d) = ((a' + c) + b') + d by RLVECT_1:def 6
.= (c + x) + d by A2, RLVECT_1:def 6
.= x + y by A3, RLVECT_1:def 6 ;
hence x + y in { (a + b) where a, b is Element of R : ( a in I & b in J ) } by A4; :: thesis: verum

end;

hence I + J is add-closed by Def1; :: thesis: verum