let G be Group; :: 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