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

x * y in N ` H

x " in N ` H

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

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

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

x " in N ` H

proof

hence
ex M being strict Subgroup of G st the carrier of M = N ` H
by A2, A4, 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 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;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