:: deftheorem Def27 defines <NAT,+> MONOID_0:def 27 :
for b₁ being non empty strict unital uniquely-decomposable SubStr of INT.Group holds
( b₁ = <NAT,+> iff the carrier of b₁ = NAT );