let G be Group; :: thesis: for H being strict Subgroup of G holds gr (carr H) = H
let H be strict Subgroup of G; :: thesis: gr (carr H) = H
for H1 being strict Subgroup of G st carr H c= the carrier of H1 holds
H is Subgroup of H1 by GROUP_2:57;
hence gr (carr H) = H by Def4; :: thesis: verum