let G be Group; :: thesis: for A, B being non empty Subset of G

for N being Subgroup of G

for x being Element of G st x in N ~ (A * B) holds

x * N meets A * B

let A, B be non empty Subset of G; :: thesis: for N being Subgroup of G

for x being Element of G st x in N ~ (A * B) holds

x * N meets A * B

let N be Subgroup of G; :: thesis: for x being Element of G st x in N ~ (A * B) holds

x * N meets A * B

let x be Element of G; :: thesis: ( x in N ~ (A * B) implies x * N meets A * B )

assume x in N ~ (A * B) ; :: thesis: x * N meets A * B

then consider x1 being Element of G such that

A1: ( x = x1 & x1 * N meets A * B ) ;

thus x * N meets A * B by A1; :: thesis: verum

for N being Subgroup of G

for x being Element of G st x in N ~ (A * B) holds

x * N meets A * B

let A, B be non empty Subset of G; :: thesis: for N being Subgroup of G

for x being Element of G st x in N ~ (A * B) holds

x * N meets A * B

let N be Subgroup of G; :: thesis: for x being Element of G st x in N ~ (A * B) holds

x * N meets A * B

let x be Element of G; :: thesis: ( x in N ~ (A * B) implies x * N meets A * B )

assume x in N ~ (A * B) ; :: thesis: x * N meets A * B

then consider x1 being Element of G such that

A1: ( x = x1 & x1 * N meets A * B ) ;

thus x * N meets A * B by A1; :: thesis: verum