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

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