for K being non empty doubleLoopStr
for v being Valuation of K st K is having_valuation holds
0. K in NonNegElements v