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)
proof
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;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in NonNegElements v or a in 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