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