Metamath Proof Explorer


Syntax definition csubmgm

Description: Class function taking a magma to its lattice of submagmas.

Ref Expression
Assertion csubmgm class SubMgm