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 Th18;
( H₁(H) c= H₁(G) & H₁( .: G,X) = H₁(G),H₃(G) .: X ) by Th18, MONOID_0:def 23;
hence H₁( .: H,X) c= H₁( .: G,X) by A1, Th17; :: according to MONOID_0:def 23 :: thesis: verum