let M be non empty multLoopStr ; :: thesis: for H1, H2 being non empty MonoidalSubStr of M st the carrier of H1 c= the carrier of H2 holds
H1 is MonoidalSubStr of H2
let H1, H2 be non empty MonoidalSubStr of M; :: thesis: ( the carrier of H1 c= the carrier of H2 implies H1 is MonoidalSubStr of H2 )
assume A1: H₁(H1) c= H₁(H2) ; :: thesis: H1 is MonoidalSubStr of H2
( H1 is SubStr of M & H2 is SubStr of M ) by Th21;
then H1 is SubStr of H2 by A1, Th28;
hence H₂(H1) c= H₂(H2) by Def23; :: according to MONOID_0:def 25 :: thesis: 1. H1 = 1. H2
H₃(H1) = H₃(M) by Def25;
hence 1. H1 = 1. H2 by Def25; :: thesis: verum