Metamath Proof Explorer


Syntax definition csubmnd

Description: Class function taking a monoid to its lattice of submonoids.

Ref Expression
Assertion csubmnd class SubMnd