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 ;
now :: thesis: for H being strict Subgroup of H1 st H = multMagma(# the carrier of N9, the multF of N9 #) holds
H 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;
hence N is normal StableSubgroup of H1 by Def10; :: thesis: verum