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
0. K in vp v
let v be Valuation of K; :: thesis: ( K is having_valuation implies 0. K in vp v )
assume A1: K is having_valuation ; :: thesis: 0. K in vp v
then vp v = { x where x is Element of K : 0 < v . x } by Def15;
hence 0. K in vp v by A1, Lm10; :: thesis: verum