let X be set ; :: thesis: for G being non empty unital multMagma
for H being non empty SubStr of G st the_unity_wrt the multF of G in the carrier of H holds
.: (H,X) is MonoidalSubStr of .: (G,X)

let G be non empty unital multMagma ; :: thesis: for H being non empty SubStr of G st the_unity_wrt the multF of G in the carrier of H holds
.: (H,X) is MonoidalSubStr of .: (G,X)

let H be non empty SubStr of G; :: thesis: ( the_unity_wrt the multF of G in the carrier of H implies .: (H,X) is MonoidalSubStr of .: (G,X) )
assume A1: the_unity_wrt the multF of G in H3(H) ; :: thesis: .: (H,X) is MonoidalSubStr of .: (G,X)
then reconsider G9 = G, H9 = H as non empty unital multMagma by MONOID_0:30;
A2: the_unity_wrt H1(H9) = the_unity_wrt H1(G9) by ;
A3: H1( .: (H,X)) = (H1(H),H3(H)) .: X by Th17;
( H1(H) c= H1(G) & H1( .: (G,X)) = (H1(G),H3(G)) .: X ) by ;
then A4: H1( .: (H,X)) c= H1( .: (G,X)) by ;
( 1. (.: (G9,X)) = X --> (the_unity_wrt H1(G)) & 1. (.: (H9,X)) = X --> (the_unity_wrt H1(H)) ) by Th22;
hence .: (H,X) is MonoidalSubStr of .: (G,X) by ; :: thesis: verum