let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: for v being Valuation of K st K is having_valuation holds
for S being Subset of (ValuatRing v) holds 0 is LowerBound of v .: S
let v be Valuation of K; :: thesis: ( K is having_valuation implies for S being Subset of (ValuatRing v) holds 0 is LowerBound of v .: S )
assume A1: K is having_valuation ; :: thesis: for S being Subset of (ValuatRing v) holds 0 is LowerBound of v .: S
let S be Subset of (ValuatRing v); :: thesis: 0 is LowerBound of v .: S
let x be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not x in v .: S or 0 <= x )
assume x in v .: S ; :: thesis: 0 <= x
then A2: ex c being Element of K st
( c in S & x = v . c ) by FUNCT_2:65;
the carrier of (ValuatRing v) = NonNegElements v by A1, Def12;
hence 0 <= x by A2, Th47; :: thesis: verum