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
( (1). H is Subgroup of G & the carrier of ((1). H) = {(1_ H)} & the carrier of ((1). G) = {(1_ G)} & 1_ H = 1_ G ) by Def7, Th53, Th65;
hence (1). H = (1). G by Th68; :: thesis: verum