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 N9 = N as Subgroup of B ;

now :: thesis: for n being Element of B holds n * N9 c= N9 * n

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in n * N9 or x in N9 * n )
assume x in n * N9 ; :: thesis: x in N9 * n
then consider a being Element of B such that
A1: x = n * a and
A2: a in N9 by GROUP_2:103;
reconsider a9 = a, n9 = n as Element of G by GROUP_2:42;
x = n9 * a9 by A1, GROUP_2:43;
then A3: x in n9 * N by A2, GROUP_2:103;
n9 * N c= N * n9 by GROUP_3:118;
then consider a1 being Element of G such that
A4: x = a1 * n9 and
A5: a1 in N by A3, GROUP_2:104;
a1 in N9 by A5;
then a1 in B by GROUP_2:40;
then reconsider a19 = a1 as Element of B ;
x = a19 * n by A4, GROUP_2:43;
hence x in N9 * n by A5, GROUP_2:104; :: thesis: verum

end;

end;

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