let K be non empty doubleLoopStr ; :: thesis: for v being Valuation of K holds NonNegElements v c= the carrier of K

let v be Valuation of K; :: thesis: NonNegElements v c= the carrier of K

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in NonNegElements v or a in the carrier of K )

assume a in NonNegElements v ; :: thesis: a in the carrier of K

then ex x being Element of K st

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

hence a in the carrier of K ; :: thesis: verum

let v be Valuation of K; :: thesis: NonNegElements v c= the carrier of K

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in NonNegElements v or a in the carrier of K )

assume a in NonNegElements v ; :: thesis: a in the carrier of K

then ex x being Element of K st

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

hence a in the carrier of K ; :: thesis: verum