let O be set ; :: thesis: for G being GroupWithOperators of O
for N being normal StableSubgroup of G
for H1 being StableSubgroup of G holds
( H1 /\ N is normal StableSubgroup of H1 & N /\ H1 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 holds
( H1 /\ N is normal StableSubgroup of H1 & N /\ H1 is normal StableSubgroup of H1 )

let N be normal StableSubgroup of G; :: thesis: for H1 being StableSubgroup of G holds
( H1 /\ N is normal StableSubgroup of H1 & N /\ H1 is normal StableSubgroup of H1 )

let H1 be StableSubgroup of G; :: thesis: ( H1 /\ N is normal StableSubgroup of H1 & N /\ H1 is normal StableSubgroup of H1 )
thus H1 /\ N is normal StableSubgroup of H1 :: thesis: N /\ H1 is normal StableSubgroup of H1
proof
reconsider A = H1 /\ N as StableSubgroup of H1 by Lm33;
now :: thesis: for H being strict Subgroup of H1 st H = multMagma(# the carrier of A, the multF of A #) holds
H is normal
reconsider N9 = 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 A, the multF of A #) implies H is normal )
assume A1: H = multMagma(# the carrier of A, the multF of A #) ; :: thesis: H is normal
now :: thesis: for b being Element of H1 holds b * H c= H * b
let b be Element of H1; :: thesis: b * H c= H * b
thus b * H c= H * b :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in b * H or x in H * b )
assume x in b * H ; :: thesis: x in H * b
then consider a being Element of H1 such that
A2: x = b * a and
A3: a in H by GROUP_2:103;
reconsider a9 = a, b9 = b as Element of G by Th2;
reconsider x9 = x as Element of H1 by A2;
A4: b9 " = b " by Th6;
a in the carrier of A by ;
then a in (carr H1) /\ (carr N) by Def25;
then a in carr N9 by XBOOLE_0:def 4;
then A5: a in N9 by STRUCT_0:def 5;
x = b9 * a9 by ;
then A6: x in b9 * N9 by ;
b9 * N9 c= N9 * b9 by GROUP_3:118;
then consider b1 being Element of G such that
A7: x = b1 * b9 and
A8: b1 in N9 by ;
reconsider x99 = x as Element of G by A7;
b1 = x99 * (b9 ") by ;
then A9: b1 = x9 * (b ") by ;
then reconsider b19 = b1 as Element of H1 ;
b1 in the carrier of N by ;
then b1 in (carr H1) /\ (carr N) by ;
then b19 in the carrier of A by Def25;
then A10: b19 in H by ;
b19 * b = x by ;
hence x in H * b by ; :: thesis: verum
end;
end;
hence H is normal by GROUP_3:118; :: thesis: verum
end;
hence H1 /\ N is normal StableSubgroup of H1 by Def10; :: thesis: verum
end;
hence N /\ H1 is normal StableSubgroup of H1 ; :: thesis: verum