let O be set ; :: thesis: for G being GroupWithOperators of O
for H, F1, F2 being strict StableSubgroup of G st F1 is normal StableSubgroup of F2 holds
H /\ F1 is normal StableSubgroup of H /\ F2
let G be GroupWithOperators of O; :: thesis: for H, F1, F2 being strict StableSubgroup of G st F1 is normal StableSubgroup of F2 holds
H /\ F1 is normal StableSubgroup of H /\ F2
let H, F1, F2 be strict StableSubgroup of G; :: thesis: ( F1 is normal StableSubgroup of F2 implies H /\ F1 is normal StableSubgroup of H /\ F2 )
reconsider F = F2 /\ H as StableSubgroup of F2 by Lm33;
assume A1: F1 is normal StableSubgroup of F2 ; :: thesis: H /\ F1 is normal StableSubgroup of H /\ F2
then A2: F1 /\ H = (F1 /\ F2) /\ H by Lm21
.= F1 /\ (F2 /\ H) by Th20 ;
reconsider F1 = F1 as normal StableSubgroup of F2 by A1;
F1 /\ F is normal StableSubgroup of F by Th41;
hence H /\ F1 is normal StableSubgroup of H /\ F2 by A2, Th39; :: thesis: verum