:: deftheorem Def6 defines NATPLUS NAT_LAT:def 6 :
for b₁ being Subset of NAT holds
( b₁ = NATPLUS iff for n being Nat holds
( n in b₁ iff 0 < n ) );