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 :: thesis: ( ( I is empty & { (a + b) where a, b is Element of R : ( a in I & b in J ) } is Subset of R ) or ( J is empty & { (a + b) where a, b is Element of R : ( a in I & b in J ) } is Subset of R ) )
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 object 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 object 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 object st x in M holds
x in the carrier of R
proof
let x be object ; :: 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