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