let X be set ; :: thesis: for G being non empty multMagma
for H being non empty SubStr of G holds .: (H,X) is SubStr of .: (G,X)
let G be non empty multMagma ; :: thesis: for H being non empty SubStr of G holds .: (H,X) is SubStr of .: (G,X)
let H be non empty SubStr of G; :: thesis: .: (H,X) is SubStr of .: (G,X)
A1: H₁( .: (H,X)) = (H₁(H),H₃(H)) .: X by Th17;
( H₁(H) c= H₁(G) & H₁( .: (G,X)) = (H₁(G),H₃(G)) .: X ) by Th17, MONOID_0:def 23;
hence H₁( .: (H,X)) c= H₁( .: (G,X)) by A1, Th16; :: according to MONOID_0:def 23 :: thesis: verum