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

let v be Valuation of K; :: thesis: ( K is having_valuation implies NonNegElements (normal-valuation v) = NonNegElements v )

assume A1: K is having_valuation ; :: thesis: NonNegElements (normal-valuation v) = NonNegElements v

set f = normal-valuation v;

thus NonNegElements (normal-valuation v) c= NonNegElements v :: according to XBOOLE_0:def 10 :: thesis: NonNegElements v c= NonNegElements (normal-valuation v)

assume a in NonNegElements v ; :: thesis: a in NonNegElements (normal-valuation v)

then consider x being Element of K such that

A4: a = x and

A5: 0 <= v . x ;

0 <= (normal-valuation v) . x by A1, A5, Th41;

hence a in NonNegElements (normal-valuation v) by A4; :: thesis: verum

NonNegElements (normal-valuation v) = NonNegElements v

let v be Valuation of K; :: thesis: ( K is having_valuation implies NonNegElements (normal-valuation v) = NonNegElements v )

assume A1: K is having_valuation ; :: thesis: NonNegElements (normal-valuation v) = NonNegElements v

set f = normal-valuation v;

thus NonNegElements (normal-valuation v) c= NonNegElements v :: according to XBOOLE_0:def 10 :: thesis: NonNegElements v c= NonNegElements (normal-valuation v)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in NonNegElements v or a in NonNegElements (normal-valuation v) )
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in NonNegElements (normal-valuation v) or a in NonNegElements v )

assume a in NonNegElements (normal-valuation v) ; :: thesis: a in NonNegElements v

then consider x being Element of K such that

A2: a = x and

A3: 0 <= (normal-valuation v) . x ;

0 <= v . x by A1, A3, Th41;

hence a in NonNegElements v by A2; :: thesis: verum

end;assume a in NonNegElements (normal-valuation v) ; :: thesis: a in NonNegElements v

then consider x being Element of K such that

A2: a = x and

A3: 0 <= (normal-valuation v) . x ;

0 <= v . x by A1, A3, Th41;

hence a in NonNegElements v by A2; :: thesis: verum

assume a in NonNegElements v ; :: thesis: a in NonNegElements (normal-valuation v)

then consider x being Element of K such that

A4: a = x and

A5: 0 <= v . x ;

0 <= (normal-valuation v) . x by A1, A5, Th41;

hence a in NonNegElements (normal-valuation v) by A4; :: thesis: verum