let G be Group; :: thesis: for N, H being Subgroup of G holds carr H c= N ~ H
let N, H be Subgroup of G; :: thesis: carr H c= N ~ H
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in carr H or x in N ~ H )
assume x in carr H ; :: thesis: x in N ~ H
then reconsider x = x as Element of H ;
reconsider x = x as Element of G by GROUP_2:42;
x in x * N by GROUP_2:108;
then x * N meets carr H by XBOOLE_0:3;
hence x in N ~ H ; :: thesis: verum