let G be Group; :: thesis: for N, H being Subgroup of G holds N ` H c= carr H
let N, H be Subgroup of G; :: thesis: N ` H c= carr H
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in N ` H or x in carr H )
assume x in N ` H ; :: thesis: x in carr H
then consider y1 being Element of G such that
A1: ( y1 = x & y1 * N c= carr H ) ;
y1 in y1 * N by GROUP_2:108;
hence x in carr H by A1; :: thesis: verum