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 N' = N as StableSubgroup of H1 ;

now

let H be strict Subgroup of H1; :: thesis: ( H = multMagma(# the carrier of N',the multF of N' #) implies H is normal )
assume A1: H = multMagma(# the carrier of N',the multF of N' #) ; :: thesis: H is normal
A2: H1 is Subgroup of G by Def7;
reconsider N'' = multMagma(# the carrier of N,the multF of N #) as normal Subgroup of G by Lm7;
reconsider N = N as Subgroup of G by Def7;
N'' is Subgroup of N by GROUP_2:66;
hence H is normal by A1, A2, GROUP_6:9; :: thesis: verum

end;

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