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