theorem Th74: :: FVALUAT1:74

for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for a being Element of K
for v being Valuation of K st K is having_valuation & v . a = 0 holds
for I being Ideal of (ValuatRing v) holds
( a in I iff I = the carrier of (ValuatRing v) )