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

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