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

least-positive (rng v) in rng v

let v be Valuation of K; :: thesis: ( K is having_valuation implies least-positive (rng v) in rng v )

assume K is having_valuation ; :: thesis: least-positive (rng v) in rng v

then +infty in rng v by Th33;

hence least-positive (rng v) in rng v by Def2; :: thesis: verum

least-positive (rng v) in rng v

let v be Valuation of K; :: thesis: ( K is having_valuation implies least-positive (rng v) in rng v )

assume K is having_valuation ; :: thesis: least-positive (rng v) in rng v

then +infty in rng v by Th33;

hence least-positive (rng v) in rng v by Def2; :: thesis: verum