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

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