theorem Th25: :: FVALUAT1:25

for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for a, b being Element of K
for v being Valuation of K st K is having_valuation & a <> 0. K & b <> 0. K & v . (a / b) <= 0 holds
0 <= v . (b / a)