let R be comRing; :: thesis: for a, b being Element of R holds
( a divides b iff {b} -Ideal c= {a} -Ideal )
let a, b be Element of R; :: thesis: ( a divides b iff {b} -Ideal c= {a} -Ideal )

now :: thesis: ( {b} -Ideal c= {a} -Ideal implies a divides b )

assume {b} -Ideal c= {a} -Ideal ; :: thesis: a divides b
then b in {a} -Ideal by IDEAL_1:66;
hence a divides b by div0; :: thesis: verum

end;

hence ( a divides b iff {b} -Ideal c= {a} -Ideal ) by div0, IDEAL_1:67; :: thesis: verum