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 emptyset ; 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
byA2; :: thesis: verum
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 emptyset ; 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
byA3; :: thesis: verum