let G be Group; :: thesis: for N, M being strict normal Subgroup of G st M is Subgroup of N holds
N ./. ((N,M) `*`) is normal Subgroup of G ./. M
let N, M be strict normal Subgroup of G; :: thesis: ( M is Subgroup of N implies N ./. ((N,M) `*`) is normal Subgroup of G ./. M )
assume A1: M is Subgroup of N ; :: thesis: N ./. ((N,M) `*`) is normal Subgroup of G ./. M
then A2: (N,M) `*` = M by Def1;
then reconsider I = M as normal Subgroup of N ;
reconsider J = N ./. ((N,M) `*`) as Subgroup of G ./. M by A1, Th34;

now

let S be Element of (G ./. M); :: thesis: S * J c= J * S
thus S * J c= J * S :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in S * J or x in J * S )
assume x in S * J ; :: thesis: x in J * S
then consider T being Element of (G ./. M) such that
A3: x = S * T and
A4: T in J by GROUP_2:103;
consider c being Element of N such that
T = c * I and
A5: T = I * c by A2, A4, Th28;
reconsider d = c as Element of G by GROUP_2:42;
consider a being Element of G such that
S = a * M and
A6: S = M * a by Th15;
set e = a * (d * (a "));
( c in N & a * (d * (a ")) = d |^ (a ") ) by Th4, STRUCT_0:def 5;
then a * (d * (a ")) in N by GROUP_5:3;
then reconsider f = a * (d * (a ")) as Element of N by STRUCT_0:def 5;
A7: M * (a * (d * (a "))) = I * f by Th2;
reconsider V = I * f as Element of J by A2, Th16;
A8: V in J by STRUCT_0:def 5;
reconsider V = V as Element of (G ./. M) by GROUP_2:42;
M * d = I * c by Th2;
then x = (M * a) * (M * d) by A3, A6, A5, Def4
.= (M * a) * ((M * d) * (1_ G)) by GROUP_2:37
.= (M * a) * ((M * d) * ((a ") * a)) by GROUP_1:def 5
.= (M * a) * (M * (d * ((a ") * a))) by GROUP_2:107
.= ((M * a) * M) * (d * ((a ") * a)) by GROUP_3:11
.= (M * (a * M)) * (d * ((a ") * a)) by GROUP_3:13
.= (M * (M * a)) * (d * ((a ") * a)) by GROUP_3:117
.= M * ((M * a) * (d * ((a ") * a))) by GROUP_2:98
.= M * (M * (a * (d * ((a ") * a)))) by GROUP_2:107
.= M * (M * (a * ((d * (a ")) * a))) by GROUP_1:def 3
.= M * (M * ((a * (d * (a "))) * a)) by GROUP_1:def 3
.= M * ((M * (a * (d * (a ")))) * a) by GROUP_2:107
.= M * (((a * (d * (a "))) * M) * a) by GROUP_3:117
.= M * ((a * (d * (a "))) * (M * a)) by GROUP_2:106
.= (M * (a * (d * (a ")))) * (M * a) by GROUP_3:12
.= V * S by A6, A7, Def4 ;
hence x in J * S by A8, GROUP_2:104; :: thesis: verum

end;

end;

hence N ./. ((N,M) `*`) is normal Subgroup of G ./. M by GROUP_3:118; :: thesis: verum