let G be multMagma ; :: thesis: for M being MonoidalSubStr of G holds M is SubStr of G
let M be MonoidalSubStr of G; :: thesis: M is SubStr of G
thus H₂(M) c= H₂(G) by Def24; :: according to MONOID_0:def 23 :: thesis: verum