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