:: deftheorem Def9 defines Pgenerator FVALUAT1:def 9 :
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
Pgenerator v = the Element of v " {(least-positive (rng v))};