:: deftheorem defines <NAT,+,0> MONOID_0:def 28 :
for b₁ being non empty strict well-unital MonoidalExtension of <NAT,+> holds
( b₁ = <NAT,+,0> iff verum );