:: deftheorem defines *+^+<0> MONOID_0:def 35 :
for D being non empty set
for b₂ being non empty strict well-unital MonoidalExtension of D *+^ holds
( b₂ = D *+^+<0> iff verum );