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

1. K in NonNegElements v

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

assume K is having_valuation ; :: thesis: 1. K in NonNegElements v

then v . (1. K) = 0 by Th17;

hence 1. K in NonNegElements v ; :: thesis: verum

1. K in NonNegElements v

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

assume K is having_valuation ; :: thesis: 1. K in NonNegElements v

then v . (1. K) = 0 by Th17;

hence 1. K in NonNegElements v ; :: thesis: verum