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 )

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

assume 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;

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