let R be comRing; :: thesis: for a being Element of R holds { (a * r) where r is Element of R : verum } is Ideal of R
let a be Element of R; :: thesis: { (a * r) where r is Element of R : verum } is Ideal of R
set M = { (a * r) where r is Element of R : verum } ;

A1: now :: thesis: for u being object st u in { (a * r) where r is Element of R : verum } holds
u in the carrier of R

let u be object ; :: thesis: ( u in { (a * r) where r is Element of R : verum } implies u in the carrier of R )
assume u in { (a * r) where r is Element of R : verum } ; :: thesis: u in the carrier of R
then ex r being Element of R st u = a * r ;
hence u in the carrier of R ; :: thesis: verum

end;

a * (1. R) in { (a * r) where r is Element of R : verum } ;
then reconsider M = { (a * r) where r is Element of R : verum } as non empty Subset of R by A1, TARSKI:def 3;
reconsider M = M as non empty Subset of R ;

A2: now :: thesis: for b, c being Element of R st b in M & c in M holds
b + c in M

let b, c be Element of R; :: thesis: ( b in M & c in M implies b + c in M )
assume that
A3: b in M and
A4: c in M ; :: thesis: b + c in M
consider r being Element of R such that
A5: a * r = b by A3;
consider s being Element of R such that
A6: a * s = c by A4;
b + c = a * (r + s) by A5, A6, VECTSP_1:def 7;
hence b + c in M ; :: thesis: verum

end;

A7: now :: thesis: for s, b being Element of R st b in M holds
s * b in M

let s, b be Element of R; :: thesis: ( b in M implies s * b in M )
assume b in M ; :: thesis: s * b in M
then consider r being Element of R such that
A8: a * r = b ;
s * b = (s * r) * a by A8, GROUP_1:def 3;
hence s * b in M ; :: thesis: verum

end;

now :: thesis: for s, b being Element of R st b in M holds
b * s in M

let s, b be Element of R; :: thesis: ( b in M implies b * s in M )
assume b in M ; :: thesis: b * s in M
then consider r being Element of R such that
A9: a * r = b ;
b * s = a * (r * s) by A9, GROUP_1:def 3;
hence b * s in M ; :: thesis: verum

end;

hence { (a * r) where r is Element of R : verum } is Ideal of R by A2, A7, Def1, Def2, Def3; :: thesis: verum