let G be Group; :: thesis: for F1 being strict Subgroup of G
for H, F2 being Subgroup of G st F1 is normal Subgroup of F2 holds
F1 /\ H is normal Subgroup of F2 /\ H
let F1 be strict Subgroup of G; :: thesis: for H, F2 being Subgroup of G st F1 is normal Subgroup of F2 holds
F1 /\ H is normal Subgroup of F2 /\ H
let H, F2 be Subgroup of G; :: thesis: ( F1 is normal Subgroup of F2 implies F1 /\ H is normal Subgroup of F2 /\ H )
reconsider F = F2 /\ H as Subgroup of F2 by GROUP_2:88;
assume A1: F1 is normal Subgroup of F2 ; :: thesis: F1 /\ H is normal Subgroup of F2 /\ H
then A2: F1 /\ H = (F1 /\ F2) /\ H by GROUP_2:89
.= F1 /\ (F2 /\ H) by GROUP_2:84 ;
reconsider F1 = F1 as normal Subgroup of F2 by A1;
F1 /\ F is normal Subgroup of F ;
hence F1 /\ H is normal Subgroup of F2 /\ H by A2, GROUP_6:3; :: thesis: verum