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