let G be Group; :: thesis: for H being Subgroup of G
for N being normal Subgroup of G st N is Subgroup of H holds
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 st N is Subgroup of H holds
ex M being strict Subgroup of G st the carrier of M = N ` H
let N be normal Subgroup of G; :: thesis: ( N is Subgroup of H implies ex M being strict Subgroup of G st the carrier of M = N ` H )
assume A1: N is Subgroup of H ; :: thesis: ex M being strict Subgroup of G st the carrier of M = N ` H
A2: 1_ G in N ` H
proof
1_ G in N by GROUP_2:46;
then A3: (1_ G) * N = carr N by GROUP_2:113;
carr N c= carr H by A1, GROUP_2:def 5;
hence 1_ G in N ` H by A3; :: thesis: verum
end;
A4: 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 ( x in N ` H & y in N ` H ) ; :: thesis: x * y in N ` H
then ( x * N c= carr H & y * N c= carr H ) by Th49;
then A5: (x * N) * (y * N) c= (carr H) * (carr H) by GROUP_3:4;
A6: (x * N) * (y * N) = (x * y) * N by Th1;
(carr H) * (carr H) = carr H by GROUP_2:76;
hence x * y in N ` H by A5, A6; :: 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 A7: x * N c= carr H by Th49;
x in x * N by GROUP_2:108;
then x in H by A7, STRUCT_0:def 5;
then x " in H by GROUP_2:51;
then A8: (x ") * H = carr H by GROUP_2:113;
(x ") * N c= (x ") * H by A1, GROUP_3:6;
hence x " in N ` H by A8; :: thesis: verum
end;
hence ex M being strict Subgroup of G st the carrier of M = N ` H by A2, A4, GROUP_2:52; :: thesis: verum