let G be Group; :: thesis: for N being Subgroup of G
for x, y being Element of G st y in x * N holds
x * N = y * N
let N be Subgroup of G; :: thesis: for x, y being Element of G st y in x * N holds
x * N = y * N
let x, y be Element of G; :: thesis: ( y in x * N implies x * N = y * N )
assume A1: y in x * N ; :: thesis: x * N = y * N
y in y * N by GROUP_2:108;
then x * N meets y * N by A1, XBOOLE_0:3;
hence x * N = y * N by GROUP_2:115; :: thesis: verum