let G be addGroup; :: thesis: for H being Subgroup of G holds - (carr H) = carr H
let H be Subgroup of G; :: thesis: - (carr H) = carr H
for g being Element of G st g in carr H holds
- g in carr H by Th75;
hence - (carr H) = carr H by Th23; :: thesis: verum