let O be set ; :: thesis: for G being GroupWithOperators of O

for N being normal StableSubgroup of G

for H1 being StableSubgroup of G st N is StableSubgroup of H1 holds

N is normal StableSubgroup of H1

let G be GroupWithOperators of O; :: thesis: for N being normal StableSubgroup of G

for H1 being StableSubgroup of G st N is StableSubgroup of H1 holds

N is normal StableSubgroup of H1

let N be normal StableSubgroup of G; :: thesis: for H1 being StableSubgroup of G st N is StableSubgroup of H1 holds

N is normal StableSubgroup of H1

let H1 be StableSubgroup of G; :: thesis: ( N is StableSubgroup of H1 implies N is normal StableSubgroup of H1 )

assume N is StableSubgroup of H1 ; :: thesis: N is normal StableSubgroup of H1

then reconsider N9 = N as StableSubgroup of H1 ;

for N being normal StableSubgroup of G

for H1 being StableSubgroup of G st N is StableSubgroup of H1 holds

N is normal StableSubgroup of H1

let G be GroupWithOperators of O; :: thesis: for N being normal StableSubgroup of G

for H1 being StableSubgroup of G st N is StableSubgroup of H1 holds

N is normal StableSubgroup of H1

let N be normal StableSubgroup of G; :: thesis: for H1 being StableSubgroup of G st N is StableSubgroup of H1 holds

N is normal StableSubgroup of H1

let H1 be StableSubgroup of G; :: thesis: ( N is StableSubgroup of H1 implies N is normal StableSubgroup of H1 )

assume N is StableSubgroup of H1 ; :: thesis: N is normal StableSubgroup of H1

then reconsider N9 = N as StableSubgroup of H1 ;

now :: thesis: for H being strict Subgroup of H1 st H = multMagma(# the carrier of N9, the multF of N9 #) holds

H is normal

hence
N is normal StableSubgroup of H1
by Def10; :: thesis: verumH is normal

reconsider N99 = multMagma(# the carrier of N, the multF of N #) as normal Subgroup of G by Lm6;

let H be strict Subgroup of H1; :: thesis: ( H = multMagma(# the carrier of N9, the multF of N9 #) implies H is normal )

assume A1: H = multMagma(# the carrier of N9, the multF of N9 #) ; :: thesis: H is normal

reconsider N = N as Subgroup of G by Def7;

( H1 is Subgroup of G & N99 is Subgroup of N ) by Def7, GROUP_2:57;

hence H is normal by A1, GROUP_6:8; :: thesis: verum

end;let H be strict Subgroup of H1; :: thesis: ( H = multMagma(# the carrier of N9, the multF of N9 #) implies H is normal )

assume A1: H = multMagma(# the carrier of N9, the multF of N9 #) ; :: thesis: H is normal

reconsider N = N as Subgroup of G by Def7;

( H1 is Subgroup of G & N99 is Subgroup of N ) by Def7, GROUP_2:57;

hence H is normal by A1, GROUP_6:8; :: thesis: verum