let G be Group; :: thesis: for H being Subgroup of G holds (1). H = (1). G
let H be Subgroup of G; :: thesis: (1). H = (1). G
A1: 1_ H = 1_ G by Th44;
( (1). H is Subgroup of G & the carrier of ((1). H) = {(1_ H)} ) by Def7, Th56;
hence (1). H = (1). G by A1, Def7; :: thesis: verum