for x being set holds
( x is Element of <NAT,+,0> iff x is Element of NAT )