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