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