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