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