theorem :: GROUP_11:13

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 * N c= A holds
x in N ` A ;