let G be strict Group; :: thesis: for N being strict normal Subgroup of G holds
( G ./. N is commutative Group iff G ` is Subgroup of N )
let N be strict normal Subgroup of G; :: thesis: ( G ./. N is commutative Group iff G ` is Subgroup of N )
thus ( G ./. N is commutative Group implies G ` is Subgroup of N ) :: thesis: ( G ` is Subgroup of N implies G ./. N is commutative Group )

proof

assume A1: G ./. N is commutative Group ; :: thesis: G ` is Subgroup of N

now

let a, b be Element of G; :: thesis: [.a,b.] in N
reconsider S = a * N, T = b * N as Element of (G ./. N) by Th16;
A2: ( [.S,T.] = 1_ (G ./. N) & 1_ (G ./. N) = carr N ) by A1, Th29, GROUP_5:40;
( S " = (a ") * N & T " = (b ") * N ) by Th30;
then A3: (S ") * (T ") = ((a ") * N) * ((b ") * N) by Def4;
( S * T = (a * N) * (b * N) & [.S,T.] = ((S ") * (T ")) * (S * T) ) by Def4, GROUP_5:19;
then [.S,T.] = (((a ") * N) * ((b ") * N)) * ((a * N) * (b * N)) by A3, Def4;
then carr N = (((a ") * N) * ((b ") * N)) * (a * (N * (b * N))) by A2, GROUP_3:11
.= (((a ") * N) * ((b ") * N)) * (a * ((N * b) * N)) by GROUP_3:15
.= (((a ") * N) * ((b ") * N)) * (a * ((b * N) * N)) by GROUP_3:140
.= (((a ") * N) * ((b ") * N)) * (a * (b * N)) by Th6
.= (((a ") * N) * ((b ") * N)) * ((a * b) * N) by GROUP_2:127
.= ((a ") * (N * ((b ") * N))) * ((a * b) * N) by GROUP_3:11
.= ((a ") * ((N * (b ")) * N)) * ((a * b) * N) by GROUP_3:15
.= ((a ") * (((b ") * N) * N)) * ((a * b) * N) by GROUP_3:140
.= ((a ") * ((b ") * N)) * ((a * b) * N) by Th6
.= (((a ") * (b ")) * N) * ((a * b) * N) by GROUP_2:127
.= ((a ") * (b ")) * (N * ((a * b) * N)) by GROUP_3:11
.= ((a ") * (b ")) * ((N * (a * b)) * N) by GROUP_3:15
.= ((a ") * (b ")) * (((a * b) * N) * N) by GROUP_3:140
.= ((a ") * (b ")) * ((a * b) * N) by Th6
.= (((a ") * (b ")) * (a * b)) * N by GROUP_2:127
.= [.a,b.] * N by GROUP_5:19 ;
hence [.a,b.] in N by GROUP_2:136; :: thesis: verum

end;

hence G ` is Subgroup of N by Th8; :: thesis: verum

end;

assume A4: G ` is Subgroup of N ; :: thesis: G ./. N is commutative Group

now

let S, T be Element of (G ./. N); :: thesis: [.S,T.] = 1_ (G ./. N)
A5: [.S,T.] = ((S ") * (T ")) * (S * T) by GROUP_5:19;
consider b being Element of G such that
A6: T = b * N and
T = N * b by Th15;
A7: T " = (b ") * N by A6, Th30;
consider a being Element of G such that
A8: S = a * N and
S = N * a by Th15;
S " = (a ") * N by A8, Th30;
then A9: (S ") * (T ") = ((a ") * N) * ((b ") * N) by A7, Def4;
[.a,b.] in N by A4, Th8;
then A10: carr N = [.a,b.] * N by GROUP_2:136
.= (((a ") * (b ")) * (a * b)) * N by GROUP_5:19
.= ((a ") * (b ")) * ((a * b) * N) by GROUP_2:127
.= ((a ") * (b ")) * (((a * b) * N) * N) by Th6
.= ((a ") * (b ")) * ((N * (a * b)) * N) by GROUP_3:140
.= ((a ") * (b ")) * (N * ((a * b) * N)) by GROUP_3:15
.= (((a ") * (b ")) * N) * ((a * b) * N) by GROUP_3:11
.= ((a ") * ((b ") * N)) * ((a * b) * N) by GROUP_2:127
.= ((a ") * (((b ") * N) * N)) * ((a * b) * N) by Th6
.= ((a ") * ((N * (b ")) * N)) * ((a * b) * N) by GROUP_3:140
.= ((a ") * (N * ((b ") * N))) * ((a * b) * N) by GROUP_3:15
.= (((a ") * N) * ((b ") * N)) * ((a * b) * N) by GROUP_3:11
.= (((a ") * N) * ((b ") * N)) * (a * (b * N)) by GROUP_2:127
.= (((a ") * N) * ((b ") * N)) * (a * ((b * N) * N)) by Th6
.= (((a ") * N) * ((b ") * N)) * (a * ((N * b) * N)) by GROUP_3:140
.= (((a ") * N) * ((b ") * N)) * (a * (N * (b * N))) by GROUP_3:15
.= (((a ") * N) * ((b ") * N)) * ((a * N) * (b * N)) by GROUP_3:11 ;
S * T = (a * N) * (b * N) by A8, A6, Def4;
then [.S,T.] = (((a ") * N) * ((b ") * N)) * ((a * N) * (b * N)) by A9, A5, Def4;
hence [.S,T.] = 1_ (G ./. N) by A10, Th29; :: thesis: verum

end;

hence G ./. N is commutative Group by GROUP_5:40; :: thesis: verum