let G be non empty multLoopStr ; 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; ( ( 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
; 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
verumproof
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 #);
(
H2(
multLoopStr(# the
carrier of
H, the
multF of
H,
e #))
c= H2(
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
;
the carrier of N = D
thus
the
carrier of
N = D
by A3;
verum
end;