theorem :: MONOID_0:44

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