theorem :: GROUP_1A:93

for G being addGroup
for H1, H2 being Subgroup of G holds 0_ H1 in H2