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
proof
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 ;
hence 1_ G in N ~ H ; :: thesis: verum
end;
A3: for x, y being Element of G st x in N ~ H & y in N ~ H holds
x * y in N ~ H
proof
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 ;
consider b being Element of G such that
A7: ( b in y * N & b in H ) by ;
( (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 ;
then a * b in carr H by STRUCT_0:def 5;
then (x * y) * N meets carr H by ;
hence x * y in N ~ H ; :: thesis: verum
end;
for x being Element of G st x in N ~ H holds
x " in N ~ H
proof
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 ;
consider a1 being Element of G such that
A10: ( a = x * a1 & a1 in N ) by ;
A11: a1 " in N by ;
a " = (a1 ") * (x ") by ;
then a " in N * (x ") by ;
then A12: a " in (x ") * N by GROUP_3:117;
a " in H by ;
then a " in carr H by STRUCT_0:def 5;
then (x ") * N meets carr H by ;
hence x " in N ~ H ; :: thesis: verum
end;
hence ex M being strict Subgroup of G st the carrier of M = N ~ H by ; :: thesis: verum