for G being non empty Group-like multMagma
for H being Subgroup of G
for h being Element of H holds h is Element of G by Th41, STRUCT_0:def 5;