let G be non empty multLoopStr ; :: thesis: for D being non empty Subset of G st ( for x, y being Element of D holds x * y in D ) & 1. G in D holds
ex H being non empty strict MonoidalSubStr of G st the carrier of H = D
let D be non empty Subset of G; :: thesis: ( ( for x, y being Element of D holds x * y in D ) & 1. G in D implies ex H being non empty strict MonoidalSubStr of G st the carrier of H = D )
assume that
A1: for x, y being Element of D holds x * y in D and
A2: 1. G in D ; :: thesis: ex H being non empty strict MonoidalSubStr of G st the carrier of H = D
thus ex H being non empty strict MonoidalSubStr of G st the carrier of H = D :: thesis: verum

proof

consider H being non empty strict SubStr of G such that
A3: the carrier of H = D by Lm5, A1;
reconsider e = 1. G as Element of H by A2, A3;
set N = multLoopStr(# the carrier of H, the multF of H,e #);
( H₂( multLoopStr(# the carrier of H, the multF of H,e #)) c= H₂(G) & ( for M being multLoopStr st G = M holds
1. multLoopStr(# the carrier of H, the multF of H,e #) = 1. M ) ) by Def23;
then reconsider N = multLoopStr(# the carrier of H, the multF of H,e #) as non empty strict MonoidalSubStr of G by Def25;
take N ; :: thesis: the carrier of N = D
thus the carrier of N = D by A3; :: thesis: verum

end;