let G be Group; :: thesis: for H being Subgroup of G

for N being normal Subgroup of G ex M being strict Subgroup of G st the carrier of M = N ~ H

let H be Subgroup of G; :: thesis: for N being normal Subgroup of G ex M being strict Subgroup of G st the carrier of M = N ~ H

let N be normal Subgroup of G; :: thesis: ex M being strict Subgroup of G st the carrier of M = N ~ H

A1: 1_ G in N ~ H

x * y in N ~ H

x " in N ~ H

for N being normal Subgroup of G ex M being strict Subgroup of G st the carrier of M = N ~ H

let H be Subgroup of G; :: thesis: for N being normal Subgroup of G ex M being strict Subgroup of G st the carrier of M = N ~ H

let N be normal Subgroup of G; :: thesis: ex M being strict Subgroup of G st the carrier of M = N ~ H

A1: 1_ G in N ~ H

proof

A3:
for x, y being Element of G st x in N ~ H & y in N ~ H holds
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

end;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

x * y in N ~ H

proof

for x being Element of G st x in N ~ H holds
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

end;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

x " in N ~ H

proof

hence
ex M being strict Subgroup of G st the carrier of M = N ~ H
by A1, A3, GROUP_2:52; :: 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

end;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