let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: for v being Valuation of K st K is having_valuation holds

not 1. K in vp v

let v be Valuation of K; :: thesis: ( K is having_valuation implies not 1. K in vp v )

assume A1: K is having_valuation ; :: thesis: not 1. K in vp v

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

assume 1. K in vp v ; :: thesis: contradiction

then ex x being Element of K st

( x = 1. K & 0 < v . x ) by A2;

hence contradiction by A1, Th17; :: thesis: verum

not 1. K in vp v

let v be Valuation of K; :: thesis: ( K is having_valuation implies not 1. K in vp v )

assume A1: K is having_valuation ; :: thesis: not 1. K in vp v

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

assume 1. K in vp v ; :: thesis: contradiction

then ex x being Element of K st

( x = 1. K & 0 < v . x ) by A2;

hence contradiction by A1, Th17; :: thesis: verum