theorem :: FVALUAT1:66

for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for v being Valuation of K st K is having_valuation holds
for I being non empty Subset of K
for x being Element of (ValuatRing v) st I is Ideal of (ValuatRing v) & x in min (I,v) holds
I = {x} -Ideal