for K being non empty doubleLoopStr
for v being Valuation of K
for a being Element of K holds
( a in NonNegElements v iff 0 <= v . a )