:: deftheorem Def31 defines <NAT,*> MONOID_0:def 31 :
for b₁ being non empty strict unital uniquely-decomposable SubStr of <REAL,*> holds
( b₁ = <NAT,*> iff the carrier of b₁ = NAT );