theorem Th42: :: GROUP_1A:88

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;