let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed 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 set such that
A3: x in I and
A4: not x in vp v by TARSKI:def 3;
A5: x is Element of K by A1, A3, Th54;
v . x = 0 by A1, A4, A3, Th80;
hence contradiction by A1, A2, A3, A5, Th77; :: thesis: verum