for K being non empty doubleLoopStr
for v being Valuation of K holds NonNegElements v c= the carrier of K