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

for x being Element of G st x * N meets carr H holds

ex y being Element of G st

( y in x * N & y in H )

let N, H be Subgroup of G; :: thesis: for x being Element of G st x * N meets carr H holds

ex y being Element of G st

( y in x * N & y in H )

let x be Element of G; :: thesis: ( x * N meets carr H implies ex y being Element of G st

( y in x * N & y in H ) )

assume x * N meets carr H ; :: thesis: ex y being Element of G st

( y in x * N & y in H )

then consider y being object such that

A1: ( y in x * N & y in carr H ) by XBOOLE_0:3;

reconsider y = y as Element of G by A1;

y in H by A1, STRUCT_0:def 5;

hence ex y being Element of G st

( y in x * N & y in H ) by A1; :: thesis: verum

for x being Element of G st x * N meets carr H holds

ex y being Element of G st

( y in x * N & y in H )

let N, H be Subgroup of G; :: thesis: for x being Element of G st x * N meets carr H holds

ex y being Element of G st

( y in x * N & y in H )

let x be Element of G; :: thesis: ( x * N meets carr H implies ex y being Element of G st

( y in x * N & y in H ) )

assume x * N meets carr H ; :: thesis: ex y being Element of G st

( y in x * N & y in H )

then consider y being object such that

A1: ( y in x * N & y in carr H ) by XBOOLE_0:3;

reconsider y = y as Element of G by A1;

y in H by A1, STRUCT_0:def 5;

hence ex y being Element of G st

( y in x * N & y in H ) by A1; :: thesis: verum