let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: for a being Element of K

for v being Valuation of K st K is having_valuation holds

( 0 <= v . a iff a is Element of (ValuatRing v) )

let a be Element of K; :: thesis: for v being Valuation of K st K is having_valuation holds

( 0 <= v . a iff a is Element of (ValuatRing v) )

let v be Valuation of K; :: thesis: ( K is having_valuation implies ( 0 <= v . a iff a is Element of (ValuatRing v) ) )

assume K is having_valuation ; :: thesis: ( 0 <= v . a iff a is Element of (ValuatRing v) )

then the carrier of (ValuatRing v) = NonNegElements v by Def12;

hence ( 0 <= v . a iff a is Element of (ValuatRing v) ) by Th47; :: thesis: verum

for v being Valuation of K st K is having_valuation holds

( 0 <= v . a iff a is Element of (ValuatRing v) )

let a be Element of K; :: thesis: for v being Valuation of K st K is having_valuation holds

( 0 <= v . a iff a is Element of (ValuatRing v) )

let v be Valuation of K; :: thesis: ( K is having_valuation implies ( 0 <= v . a iff a is Element of (ValuatRing v) ) )

assume K is having_valuation ; :: thesis: ( 0 <= v . a iff a is Element of (ValuatRing v) )

then the carrier of (ValuatRing v) = NonNegElements v by Def12;

hence ( 0 <= v . a iff a is Element of (ValuatRing v) ) by Th47; :: thesis: verum