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 y, x being Element of R st x in M holds
y * x in M

proof

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

end;

hence for b₁ being Subset of R st b₁ = I /\ J holds
b₁ is left-ideal by Def2; :: thesis: verum