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 REAL
let v be Valuation of K; :: thesis: ( K is having_valuation implies least-positive (rng v) in REAL )
assume K is having_valuation ; :: thesis: least-positive (rng v) in REAL
then least-positive (rng v) is integer by Th35;
then least-positive (rng v) in INT by INT_1:def 2;
hence least-positive (rng v) in REAL by XREAL_0:def 1; :: thesis: verum