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 H₃(H) ; :: thesis: .: H,X is MonoidalSubStr of .: G,X
then reconsider G' = G, H' = H as non empty unital multMagma by MONOID_0:32;
A2: ( H₁(H) c= H₁(G) & H₁( .: G,X) = H₁(G),H₃(G) .: X & 1. (.: G',X) = X --> (the_unity_wrt H₁(G)) & 1. (.: H',X) = X --> (the_unity_wrt H₁(H)) & the_unity_wrt H₁(H') = the_unity_wrt H₁(G') & H₁( .: H,X) = H₁(H),H₃(H) .: X ) by A1, Th18, Th23, MONOID_0:32, MONOID_0:def 23;
then H₁( .: H,X) c= H₁( .: G,X) by Th17;
hence .: H,X is MonoidalSubStr of .: G,X by A2, MONOID_0:def 25; :: thesis: verum