theorem Th79: :: FVALUAT1:79

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 proper Ideal of (ValuatRing v) holds I c= vp v