let M9 be MonoidalSubStr of M; :: thesis: M9 is MonoidalSubStr of G
A1: H3(M9) = H3(M) by Def24;
( H2(M9) c= H2(M) & H2(M) c= H2(G) ) by Def24;
hence ( H2(M9) c= H2(G) & ( for N being multLoopStr st G = N holds
H3(M9) = H3(N) ) ) by A1, Def24; :: according to MONOID_0:def 24 :: thesis: verum