per cases ( G is multLoopStr or not G is multLoopStr ) ;

suppose G is multLoopStr ; :: thesis: ex b₁ being MonoidalSubStr of G st
( b₁ is strict & not b₁ is empty )

then reconsider L = G as multLoopStr ;
for N being multLoopStr st G = N holds
1. multLoopStr(# the carrier of L, the multF of L, the OneF of L #) = 1. N ;
then reconsider M = multLoopStr(# the carrier of L, the multF of L, the OneF of L #) as MonoidalSubStr of G by Def24;
take M ; :: thesis: ( M is strict & not M is empty )
thus M is strict ; :: thesis: not M is empty
thus not the carrier of M is empty ; :: according to STRUCT_0:def 1 :: thesis: verum

end;

suppose A1: G is not multLoopStr ; :: thesis: ex b₁ being MonoidalSubStr of G st
( b₁ is strict & not b₁ is empty )

set M = the strict MonoidalExtension of G;
A2: for N being multLoopStr st G = N holds
1. the strict MonoidalExtension of G = 1. N by A1;
multMagma(# the carrier of the strict MonoidalExtension of G, the multF of the strict MonoidalExtension of G #) = multMagma(# the carrier of G, the multF of G #) by Def22;
then reconsider M = the strict MonoidalExtension of G as MonoidalSubStr of G by A2, Def24;
take M ; :: thesis: ( M is strict & not M is empty )
thus ( M is strict & not M is empty ) ; :: thesis: verum

end;

end;