let M be multMagma ; :: thesis: for A being Subset of M holds
( A is empty iff the_submagma_generated_by A is empty )
let A be Subset of M; :: thesis: ( A is empty iff the_submagma_generated_by A is empty )

hereby :: thesis: ( the_submagma_generated_by A is empty implies A is empty )

assume A1: A is empty ; :: thesis: the_submagma_generated_by A is empty
then for v, w being Element of M st v in A & w in A holds
v * w in A ;
then reconsider A9 = A as stable Subset of M by Def10;
reconsider N = multMagma(# A9,(the_mult_induced_by A9) #) as strict multSubmagma of M by Def9;
the_submagma_generated_by A is multSubmagma of N by Def12;
then the carrier of (the_submagma_generated_by A) c= the carrier of N by Def9;
hence the_submagma_generated_by A is empty by A1; :: thesis: verum

end;

assume the_submagma_generated_by A is empty ; :: thesis: A is empty
then the carrier of (the_submagma_generated_by A) = {} ;
then A c= {} by Def12;
hence A is empty ; :: thesis: verum