let G be Group; :: thesis: for A being non empty Subset of G
for N being Subgroup of G
for x being Element of G st x in N ~ (N ` A) holds
x * N meets N ` A
let A be non empty Subset of G; :: thesis: for N being Subgroup of G
for x being Element of G st x in N ~ (N ` A) holds
x * N meets N ` A
let N be Subgroup of G; :: thesis: for x being Element of G st x in N ~ (N ` A) holds
x * N meets N ` A
let x be Element of G; :: thesis: ( x in N ~ (N ` A) implies x * N meets N ` A )
assume x in N ~ (N ` A) ; :: thesis: x * N meets N ` A
then ex x1 being Element of G st
( x = x1 & x1 * N meets N ` A ) ;
hence x * N meets N ` A ; :: thesis: verum