theorem Th30: :: GROUP_11:30

for G being Group
for A being non empty Subset of G
for N being Subgroup of G
for x being Element of G st x in N ~ (N ` (N ~ A)) holds
x * N meets N ` (N ~ A)