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 set 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