:: deftheorem Def13 defines PosElements FVALUAT1:def 13 :
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for v being Valuation of K st K is having_valuation holds
PosElements v = { x where x is Element of K : 0 < v . x } ;