let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: for a being Element of K
for v being Valuation of K st K is having_valuation holds
( not v . a is negative iff not () . a is negative )

let a be Element of K; :: thesis: for v being Valuation of K st K is having_valuation holds
( not v . a is negative iff not () . a is negative )

let v be Valuation of K; :: thesis: ( K is having_valuation implies ( not v . a is negative iff not () . a is negative ) )
set f = normal-valuation v;
set l = least-positive (rng v);
assume A1: K is having_valuation ; :: thesis: ( not v . a is negative iff not () . a is negative )
then A2: v . a = (() . a) * () by Def10;
per cases ( v . a is zero or () . a is zero or ( not v . a is zero & not () . a is zero ) ) ;
suppose ( v . a is zero or () . a is zero ) ; :: thesis: ( not v . a is negative iff not () . a is negative )
thus ( not v . a is negative iff not () . a is negative ) by A2; :: thesis: verum
end;
suppose that A3: not v . a is zero and
A4: not (normal-valuation v) . a is zero ; :: thesis: ( not v . a is negative iff not () . a is negative )
thus ( not v . a is negative implies not () . a is negative ) by A1, A3, Th40; :: thesis: ( not () . a is negative implies not v . a is negative )
thus ( not (normal-valuation v) . a is negative implies not v . a is negative ) by A4, A1, Th40; :: thesis: verum
end;
end;