per cases ( G is multLoopStr or not G is multLoopStr ) ;
suppose G is multLoopStr ; :: thesis: ex b1 being MonoidalSubStr of G st
( b1 is strict & not b1 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 b1 being MonoidalSubStr of G st
( b1 is strict & not b1 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;