:: deftheorem Def12 defines the_submagma_generated_by ALGSTR_4:def 12 :
for M being multMagma
for A being Subset of M
for b₃ being strict multSubmagma of M holds
( b₃ = the_submagma_generated_by A iff ( A c= the carrier of b₃ & ( for N being strict multSubmagma of M st A c= the carrier of N holds
b₃ is multSubmagma of N ) ) );