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 that
A1: x in { (a + b) where a, b is Element of R : ( a in I & b in J ) } and
A2: 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 ) }
consider a9, b9 being Element of R such that
A3: x = a9 + b9 and
A4: ( a9 in I & b9 in J ) by A1;
consider c, d being Element of R such that
A5: y = c + d and
A6: ( c in I & d in J ) by A2;
A7: (a9 + c) + (b9 + d) = ((a9 + c) + b9) + d by RLVECT_1:def 3
.= (c + x) + d by A3, RLVECT_1:def 3
.= x + y by A5, RLVECT_1:def 3 ;
( a9 + c in I & b9 + d in J ) by A4, A6, Def1;
hence x + y in { (a + b) where a, b is Element of R : ( a in I & b in J ) } by A7; :: thesis: verum

end;

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