theorem :: LATSUBGR:14

for G being Group
for H being strict Subgroup of G holds 1_ G in (carr G) . H