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 b1 being Subset of R st b1 = I /\ J holds
b1 is left-ideal ; :: thesis: verum