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

proof

let y, x be Element of ; :: thesis: ( x in M implies y * x in M )
assume x in M ; :: thesis: y * x in M
then consider a being Element of 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 st b₁ = I /\ J holds
b₁ is left-ideal by Def2; :: thesis: verum