let G be Group; :: thesis: for H, N being Subgroup of G holds carr H c= N ~ H
let H, N be Subgroup of G; :: thesis: carr H c= N ~ H
let x be set ; :: 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:51;
x in x * N by GROUP_2:130;
then x * N meets carr H by XBOOLE_0:3;
hence x in N ~ H ; :: thesis: verum