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 H₁(H1) c= H₁(H2) ; :: thesis: H1 is SubStr of H2
then ( H₂(H1) c= H₂(G) & H₂(H2) c= H₂(G) & dom H₂(H1) = [:H₁(H1),H₁(H1):] & [:H₁(H1),H₁(H1):] c= [:H₁(H2),H₁(H2):] & dom H₂(H2) = [:H₁(H2),H₁(H2):] ) by Def23, FUNCT_2:def 1, ZFMISC_1:119;
then ( (H₂(G) || H₁(H2)) || H₁(H1) = H₂(G) || H₁(H1) & H₂(H1) = H₂(G) || H₁(H1) & H₂(H2) = H₂(G) || H₁(H2) ) by FUNCT_1:82, GRFUNC_1:64;
hence H₂(H1) c= H₂(H2) by RELAT_1:88; :: according to MONOID_0:def 23 :: thesis: verum