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
( (carr G) . H = the carrier of H & 1_ H = 1_ G ) by Def1, GROUP_2:44;
hence 1_ G in (carr G) . H ; :: thesis: verum