let K be non empty doubleLoopStr ; :: thesis: for v being Valuation of K st K is having_valuation holds

0. K in NonNegElements v

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

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

then v . (0. K) = +infty by Def8;

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

0. K in NonNegElements v

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

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

then v . (0. K) = +infty by Def8;

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