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

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