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) is integer
let v be Valuation of K; :: thesis: ( K is having_valuation implies least-positive (rng v) is integer )
set l = least-positive (rng v);
assume A1: K is having_valuation ; :: thesis: least-positive (rng v) is integer
then consider a being Element of K such that
A2: v . a <> 0 and
A3: v . a <> +infty by Def8;
A4: dom v = the carrier of K by FUNCT_2:def 1;
then A5: v . a in rng v by FUNCT_1:def 3;
assume not least-positive (rng v) is integer ; :: thesis: contradiction
then A6: least-positive (rng v) = +infty by Def1;
A7: a <> 0. K by A1, A3, Def8;
then v . a in INT by A1, Def8;
then reconsider va = v . a as Real ;

per cases ( va is positive or not va is positive ) ;

suppose va is positive ; :: thesis: contradiction

then least-positive (rng v) <= v . a by A5, Def2;
hence contradiction by A3, A6, XXREAL_0:4; :: thesis: verum

end;

suppose not va is positive ; :: thesis: contradiction

then reconsider va = va as non positive Real ;
reconsider va = va as negative Real by A2;
set b = a " ;
a " <> 0. K by A7, VECTSP_2:13;
then A8: v . (a ") in INT by A1, Def8;
A9: v . (a ") in rng v by A4, FUNCT_1:def 3;
v . (a ") = - (v . a) by A1, A7, Th21
.= - va by XXREAL_3:def 3 ;
then least-positive (rng v) <= v . (a ") by A9, Def2;
hence contradiction by A8, A6, XXREAL_0:4; :: thesis: verum

end;

end;