let G be Group; :: thesis: for H being strict Subgroup of G holds H |^ (1_ G) = H
let H be strict Subgroup of G; :: thesis: H |^ (1_ G) = H
the carrier of (H |^ (1_ G)) = (carr H) |^ (1_ G) by Def6
.= the carrier of H by Th52 ;
hence H |^ (1_ G) = H by GROUP_2:59; :: thesis: verum