theorem Th13: :: LATSUBGR:13

for G being Group
for H being strict Subgroup of G
for x being Element of G holds
( x in (carr G) . H iff x in H )