for G being non empty multMagma
for H being non empty SubStr of G st G is unital & the_unity_wrt the multF of G in the carrier of H holds
( H is unital & the_unity_wrt the multF of G = the_unity_wrt the multF of H )