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 c= carr H
let N, H be Subgroup of G; :: thesis: for x being Element of G st x in N ` H holds
x * N c= carr H
let x be Element of G; :: thesis: ( x in N ` H implies x * N c= carr H )
assume x in N ` H ; :: thesis: x * N c= carr H
then ex x1 being Element of G st
( x1 = x & x1 * N c= carr H ) ;
hence x * N c= carr H ; :: thesis: verum