theorem div1: :: RING_2:19
for R being comRing
for a, b being Element of R holds
( a divides b iff {b} -Ideal c= {a} -Ideal )