for G being Group
for H being strict Subgroup of G holds (carr G) . H <> {} by Def1;