1_ G in H by GROUP_2:46;
then A2: 1_ G in carr H by STRUCT_0:def 5;
1_ G in (1_ G) * N by GROUP_2:108;
then (1_ G) * N meets carr H by A2, XBOOLE_0:3;
hence 1_ G in N ~ H ; :: thesis: verum

let x, y be Element of G; :: thesis: ( x in N ~ H & y in N ~ H implies x * y in N ~ H )
assume that
A4: x in N ~ H and
A5: y in N ~ H ; :: thesis: x * y in N ~ H
consider a being Element of G such that
A6: ( a in x * N & a in H ) by A4, Th51, Th3;
consider b being Element of G such that
A7: ( b in y * N & b in H ) by A5, Th51, Th3;
( (x * N) * (y * N) = (x * y) * N & (a * N) * (b * N) = (a * b) * N ) by Th1;
then A8: a * b in (x * y) * N by A6, A7;
a * b in H by A6, A7, GROUP_2:50;
then a * b in carr H by STRUCT_0:def 5;
then (x * y) * N meets carr H by A8, XBOOLE_0:3;
hence x * y in N ~ H ; :: thesis: verum

let x be Element of G; :: thesis: ( x in N ~ H implies x " in N ~ H )
assume x in N ~ H ; :: thesis: x " in N ~ H
then consider a being Element of G such that
A9: ( a in x * N & a in H ) by Th3, Th51;
consider a1 being Element of G such that
A10: ( a = x * a1 & a1 in N ) by A9, GROUP_2:103;
A11: a1 " in N by A10, GROUP_2:51;
a " = (a1 ") * (x ") by A10, GROUP_1:17;
then a " in N * (x ") by A11, GROUP_2:104;
then A12: a " in (x ") * N by GROUP_3:117;
a " in H by A9, GROUP_2:51;
then a " in carr H by STRUCT_0:def 5;
then (x ") * N meets carr H by A12, XBOOLE_0:3;
hence x " in N ~ H ; :: thesis: verum