let G be Group; :: thesis: for H being strict Subgroup of G holds 1_ G in (carr G) . H
let H be strict Subgroup of G; :: thesis: 1_ G in (carr G) . H
A1: (carr G) . H = the carrier of H by Def1;
1_ H = 1_ G by GROUP_2:53;
hence 1_ G in (carr G) . H by A1; :: thesis: verum