theorem Th65: :: FVALUAT1:65

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
for S being non empty Subset of K st K is having_valuation & S is Subset of (ValuatRing v) holds
for x being Element of K holds
( x in min (S,v) iff ( x in S & ( for y being Element of K st y in S holds
v . x <= v . y ) ) )