let G be Group; :: thesis: for H, N being normal Subgroup of G st N is Subgroup of H holds

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

let H, N be normal Subgroup of G; :: thesis: ( N is Subgroup of H implies ex M being strict normal Subgroup of G st the carrier of M = N ` H )

assume A1: N is Subgroup of H ; :: thesis: ex M being strict normal Subgroup of G st the carrier of M = N ` H

then consider M being strict Subgroup of G such that

A2: the carrier of M = N ` H by Th72;

for x being Element of G holds x * M c= M * x

hence ex M being strict normal Subgroup of G st the carrier of M = N ` H by A2; :: thesis: verum

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

let H, N be normal Subgroup of G; :: thesis: ( N is Subgroup of H implies ex M being strict normal Subgroup of G st the carrier of M = N ` H )

assume A1: N is Subgroup of H ; :: thesis: ex M being strict normal Subgroup of G st the carrier of M = N ` H

then consider M being strict Subgroup of G such that

A2: the carrier of M = N ` H by Th72;

for x being Element of G holds x * M c= M * x

proof

then
M is normal Subgroup of G
by GROUP_3:118;
let x be Element of G; :: thesis: x * M c= M * x

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in x * M or y in M * x )

assume A3: y in x * M ; :: thesis: y in M * x

then reconsider y = y as Element of G ;

consider z being Element of G such that

A4: ( y = x * z & z in M ) by A3, GROUP_2:103;

z in the carrier of M by A4, STRUCT_0:def 5;

then A5: z * N c= carr H by A2, Th49;

z in z * N by GROUP_2:108;

then z in H by A5, STRUCT_0:def 5;

then (x * z) * (x ") in H by Th4;

then A6: ((x * z) * (x ")) * H = carr H by GROUP_2:113;

((x * z) * (x ")) * N c= ((x * z) * (x ")) * H by A1, GROUP_3:6;

then (x * z) * (x ") in N ` H by A6;

then A7: (x * z) * (x ") in M by A2, STRUCT_0:def 5;

((x * z) * (x ")) * x = y by A4, GROUP_3:1;

hence y in M * x by A7, GROUP_2:104; :: thesis: verum

end;let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in x * M or y in M * x )

assume A3: y in x * M ; :: thesis: y in M * x

then reconsider y = y as Element of G ;

consider z being Element of G such that

A4: ( y = x * z & z in M ) by A3, GROUP_2:103;

z in the carrier of M by A4, STRUCT_0:def 5;

then A5: z * N c= carr H by A2, Th49;

z in z * N by GROUP_2:108;

then z in H by A5, STRUCT_0:def 5;

then (x * z) * (x ") in H by Th4;

then A6: ((x * z) * (x ")) * H = carr H by GROUP_2:113;

((x * z) * (x ")) * N c= ((x * z) * (x ")) * H by A1, GROUP_3:6;

then (x * z) * (x ") in N ` H by A6;

then A7: (x * z) * (x ") in M by A2, STRUCT_0:def 5;

((x * z) * (x ")) * x = y by A4, GROUP_3:1;

hence y in M * x by A7, GROUP_2:104; :: thesis: verum

hence ex M being strict normal Subgroup of G st the carrier of M = N ` H by A2; :: thesis: verum