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$ |