let K be non empty doubleLoopStr ; :: thesis: for v being Valuation of K

for a being Element of K holds

( a in NonNegElements v iff 0 <= v . a )

let v be Valuation of K; :: thesis: for a being Element of K holds

( a in NonNegElements v iff 0 <= v . a )

let a be Element of K; :: thesis: ( a in NonNegElements v iff 0 <= v . a )

for a being Element of K holds

( a in NonNegElements v iff 0 <= v . a )

let v be Valuation of K; :: thesis: for a being Element of K holds

( a in NonNegElements v iff 0 <= v . a )

let a be Element of K; :: thesis: ( a in NonNegElements v iff 0 <= v . a )

hereby :: thesis: ( 0 <= v . a implies a in NonNegElements v )

thus
( 0 <= v . a implies a in NonNegElements v )
; :: thesis: verumassume
a in NonNegElements v
; :: thesis: 0 <= v . a

then ex x being Element of K st

( a = x & 0 <= v . x ) ;

hence 0 <= v . a ; :: thesis: verum

end;then ex x being Element of K st

( a = x & 0 <= v . x ) ;

hence 0 <= v . a ; :: thesis: verum