let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: 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)

let a, b be Element of K; :: thesis: 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)

let v be Valuation of K; :: thesis: ( K is having_valuation & a <> 0. K & b <> 0. K & v . (a / b) <= 0 implies 0 <= v . (b / a) )

assume ( K is having_valuation & a <> 0. K & b <> 0. K ) ; :: thesis: ( not v . (a / b) <= 0 or 0 <= v . (b / a) )

then v . (a / b) = - (v . (b / a)) by Th23;

hence ( not v . (a / b) <= 0 or 0 <= v . (b / a) ) ; :: thesis: verum

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)

let a, b be Element of K; :: thesis: 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)

let v be Valuation of K; :: thesis: ( K is having_valuation & a <> 0. K & b <> 0. K & v . (a / b) <= 0 implies 0 <= v . (b / a) )

assume ( K is having_valuation & a <> 0. K & b <> 0. K ) ; :: thesis: ( not v . (a / b) <= 0 or 0 <= v . (b / a) )

then v . (a / b) = - (v . (b / a)) by Th23;

hence ( not v . (a / b) <= 0 or 0 <= v . (b / a) ) ; :: thesis: verum