set M = { x where x is Element of R : ( x in I & x in J ) } ;
{ x where x is Element of R : ( x in I & x in J ) } = I /\ J ;
then reconsider M = { x where x is Element of R : ( x in I & x in J ) } as Subset of R ;
for x, y being Element of R st x in M & y in M holds
x + y in M

proof

let x, y be Element of R; :: thesis: ( x in M & y in M implies x + y in M )
assume A1: ( x in M & y in M ) ; :: thesis: x + y in M
then consider a being Element of R such that
A2: ( x = a & a in I & a in J ) ;
consider c being Element of R such that
A3: ( c = y & c in I & c in J ) by A1;
( a + c in I & a + c in J ) by A2, A3, Def1;
hence x + y in M by A2, A3; :: thesis: verum

end;

hence for b₁ being Subset of R st b₁ = I /\ J holds
b₁ is add-closed by Def1; :: thesis: verum