## Submonoid

### Meta

 context $\langle\!\langle M,*\rangle\!\rangle$ … monoid definiendum $\langle\!\langle S,*\rangle\!\rangle\in$ it inclusion $S\in$ closed monoid subset of $\langle\!\langle M,*\rangle\!\rangle$ exists $e\in S$ postulate $e$ … unit of $\langle\!\langle M,*\rangle\!\rangle$