theorem Th58: :: GROUP_1A:104

for G being addGroup
for H1, H2 being Subgroup of G st ( for g being Element of G st g in H1 holds
g in H2 ) holds
H1 is Subgroup of H2