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

assume A5: a = 0. K ; :: thesis: contradiction
a / b = a * (b ")
.= 0. K by A5, VECTSP_1:6 ;
hence contradiction by A1, Def10, A3; :: thesis: verum

end;

then 0 <= v . (b / a) by A1, A2, A3, Th26;
hence v . a <= v . b by A1, A4, Th25; :: thesis: verum