let N be SubStr of M; :: thesis: N is SubStr of G
multMagma(# the carrier of M, the multF of M #) = multMagma(# the carrier of G, the multF of G #) by Def22;
hence H₂(N) c= H₂(G) by Def23; :: according to MONOID_0:def 23 :: thesis: verum