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

( a in vp v iff 0 < v . a )

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

( a in vp v iff 0 < v . a )

let v be Valuation of K; :: thesis: ( K is having_valuation implies ( a in vp v iff 0 < v . a ) )

assume K is having_valuation ; :: thesis: ( a in vp v iff 0 < v . a )

then A1: vp v = { x where x is Element of K : 0 < v . x } by Def13;

for v being Valuation of K st K is having_valuation holds

( a in vp v iff 0 < v . a )

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

( a in vp v iff 0 < v . a )

let v be Valuation of K; :: thesis: ( K is having_valuation implies ( a in vp v iff 0 < v . a ) )

assume K is having_valuation ; :: thesis: ( a in vp v iff 0 < v . a )

then A1: vp v = { x where x is Element of K : 0 < v . x } by Def13;

hereby :: thesis: ( 0 < v . a implies a in vp v )

thus
( 0 < v . a implies a in vp v )
by A1; :: thesis: verumassume
a in vp v
; :: thesis: 0 < v . a

then ex b being Element of K st

( b = a & 0 < v . b ) by A1;

hence 0 < v . a ; :: thesis: verum

end;then ex b being Element of K st

( b = a & 0 < v . b ) by A1;

hence 0 < v . a ; :: thesis: verum