Submonoid

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$