:: deftheorem defines NonNegElements FVALUAT1:def 11 :
for K being non empty doubleLoopStr
for v being Valuation of K holds NonNegElements v = { x where x is Element of K : 0 <= v . x } ;