let G be addGroup; :: thesis: for H1, H2 being Subgroup of G holds 0_ H1 in H2
let H1, H2 be Subgroup of G; :: thesis: 0_ H1 in H2
0_ H1 = 0_ G by Th44;
hence 0_ H1 in H2 by Th46; :: thesis: verum