theorem Th108: :: GROUP_1A:307

for G being addGroup
for g being Element of G
for H being strict Subgroup of G holds H * g in con_class H