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

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