set M = { (a + b) where a, b is Element of R : ( a in I & b in J ) } ;
{ (a + b) where a, b is Element of R : ( a in I & b in J ) } is Subset of R

proof

per cases ( I is empty or J is empty or ( not I is empty & not J is empty ) ) ;

suppose A1: ( I is empty or J is empty ) ; :: thesis: { (a + b) where a, b is Element of R : ( a in I & b in J ) } is Subset of R

now

per cases ( I is empty or J is empty ) by A1;

case A2: I is empty ; :: thesis: { (a + b) where a, b is Element of R : ( a in I & b in J ) } is Subset of R

{ (a + b) where a, b is Element of R : ( a in I & b in J ) } is empty

proof

assume not { (a + b) where a, b is Element of R : ( a in I & b in J ) } is empty ; :: thesis: contradiction
then reconsider M = { (a + b) where a, b is Element of R : ( a in I & b in J ) } as non empty set ;
set x = the Element of M;
the Element of M in { (a + b) where a, b is Element of R : ( a in I & b in J ) } ;
then ex a, b being Element of R st
( the Element of M = a + b & a in I & b in J ) ;
hence contradiction by A2; :: thesis: verum

end;

then for u being set st u in { (a + b) where a, b is Element of R : ( a in I & b in J ) } holds
u in the carrier of R ;
hence { (a + b) where a, b is Element of R : ( a in I & b in J ) } is Subset of R by TARSKI:def 3; :: thesis: verum

end;

case A3: J is empty ; :: thesis: { (a + b) where a, b is Element of R : ( a in I & b in J ) } is Subset of R

{ (a + b) where a, b is Element of R : ( a in I & b in J ) } is empty

proof

assume not { (a + b) where a, b is Element of R : ( a in I & b in J ) } is empty ; :: thesis: contradiction
then reconsider M = { (a + b) where a, b is Element of R : ( a in I & b in J ) } as non empty set ;
set x = the Element of M;
the Element of M in { (a + b) where a, b is Element of R : ( a in I & b in J ) } ;
then ex a, b being Element of R st
( the Element of M = a + b & a in I & b in J ) ;
hence contradiction by A3; :: thesis: verum

end;

then for u being set st u in { (a + b) where a, b is Element of R : ( a in I & b in J ) } holds
u in the carrier of R ;
hence { (a + b) where a, b is Element of R : ( a in I & b in J ) } is Subset of R by TARSKI:def 3; :: thesis: verum

end;

end;

end;

hence { (a + b) where a, b is Element of R : ( a in I & b in J ) } is Subset of R ; :: thesis: verum

end;

suppose A4: ( not I is empty & not J is empty ) ; :: thesis: { (a + b) where a, b is Element of R : ( a in I & b in J ) } is Subset of R

then reconsider J = J as non empty set ;
reconsider I = I as non empty set by A4;
set x9 = the Element of I;
set y9 = the Element of J;
( the Element of I in I & the Element of J in J ) ;
then reconsider x = the Element of I, y = the Element of J as Element of R ;
x + y in { (a + b) where a, b is Element of R : ( a in I & b in J ) } ;
then reconsider M = { (a + b) where a, b is Element of R : ( a in I & b in J ) } as non empty set ;
for x being set st x in M holds
x in the carrier of R

proof

let x be set ; :: thesis: ( x in M implies x in the carrier of R )
assume x in M ; :: thesis: x in the carrier of R
then ex a, b being Element of R st
( x = a + b & a in I & b in J ) ;
hence x in the carrier of R ; :: thesis: verum

end;

hence { (a + b) where a, b is Element of R : ( a in I & b in J ) } is Subset of R by TARSKI:def 3; :: thesis: verum

end;

end;

end;

hence { (a + b) where a, b is Element of R : ( a in I & b in J ) } is Subset of R ; :: thesis: verum