let G be Group; :: thesis: for N, H being Subgroup of G

for x being Element of G st x in N ~ H holds

x * N meets carr H

let N, H be Subgroup of G; :: thesis: for x being Element of G st x in N ~ H holds

x * N meets carr H

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

assume x in N ~ H ; :: thesis: x * N meets carr H

then ex x1 being Element of G st

( x = x1 & x1 * N meets carr H ) ;

hence x * N meets carr H ; :: thesis: verum

for x being Element of G st x in N ~ H holds

x * N meets carr H

let N, H be Subgroup of G; :: thesis: for x being Element of G st x in N ~ H holds

x * N meets carr H

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

assume x in N ~ H ; :: thesis: x * N meets carr H

then ex x1 being Element of G st

( x = x1 & x1 * N meets carr H ) ;

hence x * N meets carr H ; :: thesis: verum