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 ;
consider x being Element of M;
x 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
A3: ( x = a + b & a in I & b in J ) ;
thus contradiction by A2, 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;

case A4: 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 ;
consider x being Element of M;
x 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
A5: ( x = a + b & a in I & b in J ) ;
thus contradiction by A4, A5; :: 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 A6: ( 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 I = I as non empty set ;
reconsider J = J as non empty set by A6;
consider x' being Element of I;
consider y' being Element of J;
( x' in I & y' in J ) ;
then reconsider x = x', y = y' 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 consider a, b being Element of R such that
A7: ( x = a + b & a in I & b in J ) ;
thus x in the carrier of R by A7; :: 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