theorem div2: :: RING_2:20
for R being comRing
for a being Element of R holds
( a is Unit of R iff {a} -Ideal = [#] R )