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