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

proof

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

end;

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