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 & b <> 0. K & v . (a / b) <= 0 holds

v . a <= v . b

let a, b be Element of K; :: thesis: for v being Valuation of K st K is having_valuation & b <> 0. K & v . (a / b) <= 0 holds

v . a <= v . b

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

assume that

A1: K is having_valuation and

A2: b <> 0. K and

A3: v . (a / b) <= 0 ; :: thesis: v . a <= v . b

A4: a <> 0. K by A1, Def8, A3;

then 0 <= v . (b / a) by A1, A2, A3, Th25;

hence v . a <= v . b by A1, A4, Th24; :: thesis: verum

for v being Valuation of K st K is having_valuation & b <> 0. K & v . (a / b) <= 0 holds

v . a <= v . b

let a, b be Element of K; :: thesis: for v being Valuation of K st K is having_valuation & b <> 0. K & v . (a / b) <= 0 holds

v . a <= v . b

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

assume that

A1: K is having_valuation and

A2: b <> 0. K and

A3: v . (a / b) <= 0 ; :: thesis: v . a <= v . b

A4: a <> 0. K by A1, Def8, A3;

then 0 <= v . (b / a) by A1, A2, A3, Th25;

hence v . a <= v . b by A1, A4, Th24; :: thesis: verum