set M = { a where a is Element of R : a * J c= I } ;
{ a where a is Element of R : a * J c= I } = I % J ;
then reconsider M = { a where a is Element of R : a * J c= I } as non empty 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 * J c= I ;

now :: thesis: for u being object st u in (y * a) * J holds
u in I

let u be object ; :: thesis: ( u in (y * a) * J implies u in I )
assume u in (y * a) * J ; :: thesis: u in I
then consider c being Element of R such that
A3: u = (y * a) * c and
A4: c in J ;
y * c in J by A4, Def2;
then A5: a * (y * c) in { (a * i) where i is Element of R : i in J } ;
u = a * (y * c) by A3, GROUP_1:def 3;
hence u in I by A2, A5; :: thesis: verum

end;

then (y * a) * J c= I ;
hence y * x in M by A1; :: thesis: verum

end;

hence I % J is left-ideal ; :: thesis: verum