let G be non empty multMagma ; :: thesis: for H1, H2 being non empty SubStr of G st the carrier of H1 c= the carrier of H2 holds
H1 is SubStr of H2
let H1, H2 be non empty SubStr of G; :: thesis: ( the carrier of H1 c= the carrier of H2 implies H1 is SubStr of H2 )
assume H1(H1) c= H1(H2) ; :: thesis: H1 is SubStr of H2
then [:H1(H1),H1(H1):] c= [:H1(H2),H1(H2):] by ZFMISC_1:96;
then A1: (H2(G) || H1(H2)) || H1(H1) = H2(G) || H1(H1) by FUNCT_1:51;
( H2(H2) c= H2(G) & dom H2(H2) = [:H1(H2),H1(H2):] ) by Def23, FUNCT_2:def 1;
then A2: H2(H2) = H2(G) || H1(H2) by GRFUNC_1:23;
( H2(H1) c= H2(G) & dom H2(H1) = [:H1(H1),H1(H1):] ) by Def23, FUNCT_2:def 1;
then H2(H1) = H2(G) || H1(H1) by GRFUNC_1:23;
hence H2(H1) c= H2(H2) by A1, A2, RELAT_1:59; :: according to MONOID_0:def 23 :: thesis: verum