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;

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

assume 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;

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