let G be Group; :: thesis: for A being Subset of G
for H being strict Subgroup of G st A = the carrier of H holds
gr A = H
let A be Subset of G; :: thesis: for H being strict Subgroup of G st A = the carrier of H holds
gr A = H
let H be strict Subgroup of G; :: thesis: ( A = the carrier of H implies gr A = H )
assume A1: A = the carrier of H ; :: thesis: gr A = H
gr (carr H) = H by GROUP_4:31;
hence gr A = H by A1, GROUP_2:def 9; :: thesis: verum