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

0 <= v . a

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

0 <= v . a

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

assume that

A1: K is having_valuation and

A2: 0 <= v . ((1. K) - a) ; :: thesis: 0 <= v . a

( (1. K) - a = (1. K) + (- a) & v . (- a) = v . a ) by A1, Th20;

hence 0 <= v . a by A1, A2, Th30; :: thesis: verum

for v being Valuation of K st K is having_valuation & 0 <= v . ((1. K) - a) holds

0 <= v . a

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

0 <= v . a

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

assume that

A1: K is having_valuation and

A2: 0 <= v . ((1. K) - a) ; :: thesis: 0 <= v . a

( (1. K) - a = (1. K) + (- a) & v . (- a) = v . a ) by A1, Th20;

hence 0 <= v . a by A1, A2, Th30; :: thesis: verum