theorem Th3: :: GROUP_11:3

for G being Group
for N, H being Subgroup of G
for x being Element of G st x * N meets carr H holds
ex y being Element of G st
( y in x * N & y in H )