for A being non degenerated commutative Ring
for J being proper Ideal of A st ( for x being object st x in ([#] A) \ J holds
x is Unit of A ) holds
A is local