let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: 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
let v be Valuation of K; :: thesis: ( K is having_valuation implies for I being proper Ideal of (ValuatRing v) holds I c= vp v )
assume A1: K is having_valuation ; :: thesis: for I being proper Ideal of (ValuatRing v) holds I c= vp v
let I be proper Ideal of (ValuatRing v); :: thesis: I c= vp v
A2: I <> the carrier of (ValuatRing v) by SUBSET_1:def 6;
assume not I c= vp v ; :: thesis: contradiction
then consider x being object such that
A3: x in I and
A4: not x in vp v ;
A5: x is Element of K by A1, A3, Th51;
v . x = 0 by A1, A4, A3, Th77;
hence contradiction by A1, A2, A3, A5, Th74; :: thesis: verum