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