consider N being MonoidalSubStr of G;
H₃( multLoopStr(# the carrier of N,the multF of N,the OneF of N #)) = H₃(N) ;
then A1: for M being multLoopStr st G = M holds
H₃( multLoopStr(# the carrier of N,the multF of N,the OneF of N #)) = H₃(M) by Def24;
H₂( multLoopStr(# the carrier of N,the multF of N,the OneF of N #)) c= H₂(G) by Def24;
then multLoopStr(# the carrier of N,the multF of N,the OneF of N #) is MonoidalSubStr of G by A1, Def24;
hence ex b₁ being MonoidalSubStr of G st b₁ is strict ; :: thesis: verum