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 ` (N ~ A)) holds

x * N meets N ` (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 ` (N ~ A)) holds

x * N meets N ` (N ~ A)

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

x * N meets N ` (N ~ A)

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

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

then ex x1 being Element of G st

( x = x1 & x1 * N meets N ` (N ~ A) ) ;

hence x * N meets N ` (N ~ A) ; :: thesis: verum

for N being Subgroup of G

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

x * N meets N ` (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 ` (N ~ A)) holds

x * N meets N ` (N ~ A)

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

x * N meets N ` (N ~ A)

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

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

then ex x1 being Element of G st

( x = x1 & x1 * N meets N ` (N ~ A) ) ;

hence x * N meets N ` (N ~ A) ; :: thesis: verum