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
NonNegElements () = NonNegElements v

let v be Valuation of K; :: thesis: ( K is having_valuation implies NonNegElements () = NonNegElements v )
assume A1: K is having_valuation ; :: thesis:
set f = normal-valuation v;
thus NonNegElements () c= NonNegElements v :: according to XBOOLE_0:def 10 :: thesis:
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in NonNegElements () or a in NonNegElements v )
assume a in NonNegElements () ; :: thesis:
then consider x being Element of K such that
A2: a = x and
A3: 0 <= () . x ;
0 <= v . x by A1, A3, Th41;
hence a in NonNegElements v by A2; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in NonNegElements v or a in NonNegElements () )
assume a in NonNegElements v ; :: thesis:
then consider x being Element of K such that
A4: a = x and
A5: 0 <= v . x ;
0 <= () . x by A1, A5, Th41;
hence a in NonNegElements () by A4; :: thesis: verum