theorem Th2: :: GROUP_11:2

for G being Group
for N being Subgroup of G
for x, y being Element of G st y in x * N holds
x * N = y * N