let G be Group; :: thesis: for B being Subgroup of G
for N being normal Subgroup of G st N is Subgroup of B holds
N is normal Subgroup of B
let B be Subgroup of G; :: thesis: for N being normal Subgroup of G st N is Subgroup of B holds
N is normal Subgroup of B
let N be normal Subgroup of G; :: thesis: ( N is Subgroup of B implies N is normal Subgroup of B )
assume N is Subgroup of B ; :: thesis: N is normal Subgroup of B
then reconsider N' = N as Subgroup of B ;

now

let n be Element of B; :: thesis: n * N' c= N' * n
thus n * N' c= N' * n :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in n * N' or x in N' * n )
assume x in n * N' ; :: thesis: x in N' * n
then consider a being Element of B such that
A1: x = n * a and
A2: a in N' by GROUP_2:125;
reconsider a' = a, n' = n as Element of G by GROUP_2:51;
x = n' * a' by A1, GROUP_2:52;
then ( x in n' * N & n' * N c= N * n' ) by A2, GROUP_2:125, GROUP_3:141;
then consider a1 being Element of G such that
A3: x = a1 * n' and
A4: a1 in N by GROUP_2:126;
a1 in N' by A4;
then a1 in B by GROUP_2:49;
then reconsider a1' = a1 as Element of B by STRUCT_0:def 5;
x = a1' * n by A3, GROUP_2:52;
hence x in N' * n by A4, GROUP_2:126; :: thesis: verum

end;

end;

hence N is normal Subgroup of B by GROUP_3:141; :: thesis: verum