let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed 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 Th38;
then least-positive (rng v) in INT by INT_1:def 2;
hence least-positive (rng v) in REAL ; :: thesis: verum