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 :: thesis: for a, b being Element of G holds [.a,b.] in N

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 Th14;
A2: ( [.S,T.] = 1_ (G ./. N) & 1_ (G ./. N) = carr N ) by A1, Th24, GROUP_5:37;
( S " = (a ") * N & T " = (b ") * N ) by Th25;
then A3: (S ") * (T ") = ((a ") * N) * ((b ") * N) by Def3;
( S * T = (a * N) * (b * N) & [.S,T.] = ((S ") * (T ")) * (S * T) ) by Def3, GROUP_5:16;
then [.S,T.] = (((a ") * N) * ((b ") * N)) * ((a * N) * (b * N)) by A3, Def3;
then carr N = (((a ") * N) * ((b ") * N)) * (a * (N * (b * N))) by A2, GROUP_3:10
.= (((a ") * N) * ((b ") * N)) * (a * ((N * b) * N)) by GROUP_3:13
.= (((a ") * N) * ((b ") * N)) * (a * ((b * N) * N)) by GROUP_3:117
.= (((a ") * N) * ((b ") * N)) * (a * (b * N)) by Th5
.= (((a ") * N) * ((b ") * N)) * ((a * b) * N) by GROUP_2:105
.= ((a ") * (N * ((b ") * N))) * ((a * b) * N) by GROUP_3:10
.= ((a ") * ((N * (b ")) * N)) * ((a * b) * N) by GROUP_3:13
.= ((a ") * (((b ") * N) * N)) * ((a * b) * N) by GROUP_3:117
.= ((a ") * ((b ") * N)) * ((a * b) * N) by Th5
.= (((a ") * (b ")) * N) * ((a * b) * N) by GROUP_2:105
.= ((a ") * (b ")) * (N * ((a * b) * N)) by GROUP_3:10
.= ((a ") * (b ")) * ((N * (a * b)) * N) by GROUP_3:13
.= ((a ") * (b ")) * (((a * b) * N) * N) by GROUP_3:117
.= ((a ") * (b ")) * ((a * b) * N) by Th5
.= (((a ") * (b ")) * (a * b)) * N by GROUP_2:105
.= [.a,b.] * N by GROUP_5:16 ;
hence [.a,b.] in N by GROUP_2:113; :: thesis: verum

end;

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

end;

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

now :: thesis: for S, T being Element of (G ./. N) holds [.S,T.] = 1_ (G ./. N)

let S, T be Element of (G ./. N); :: thesis: [.S,T.] = 1_ (G ./. N)
A5: [.S,T.] = ((S ") * (T ")) * (S * T) by GROUP_5:16;
consider b being Element of G such that
A6: T = b * N and
T = N * b by Th13;
A7: T " = (b ") * N by A6, Th25;
consider a being Element of G such that
A8: S = a * N and
S = N * a by Th13;
S " = (a ") * N by A8, Th25;
then A9: (S ") * (T ") = ((a ") * N) * ((b ") * N) by A7, Def3;
[.a,b.] in N by A4, Th7;
then A10: carr N = [.a,b.] * N by GROUP_2:113
.= (((a ") * (b ")) * (a * b)) * N by GROUP_5:16
.= ((a ") * (b ")) * ((a * b) * N) by GROUP_2:105
.= ((a ") * (b ")) * (((a * b) * N) * N) by Th5
.= ((a ") * (b ")) * ((N * (a * b)) * N) by GROUP_3:117
.= ((a ") * (b ")) * (N * ((a * b) * N)) by GROUP_3:13
.= (((a ") * (b ")) * N) * ((a * b) * N) by GROUP_3:10
.= ((a ") * ((b ") * N)) * ((a * b) * N) by GROUP_2:105
.= ((a ") * (((b ") * N) * N)) * ((a * b) * N) by Th5
.= ((a ") * ((N * (b ")) * N)) * ((a * b) * N) by GROUP_3:117
.= ((a ") * (N * ((b ") * N))) * ((a * b) * N) by GROUP_3:13
.= (((a ") * N) * ((b ") * N)) * ((a * b) * N) by GROUP_3:10
.= (((a ") * N) * ((b ") * N)) * (a * (b * N)) by GROUP_2:105
.= (((a ") * N) * ((b ") * N)) * (a * ((b * N) * N)) by Th5
.= (((a ") * N) * ((b ") * N)) * (a * ((N * b) * N)) by GROUP_3:117
.= (((a ") * N) * ((b ") * N)) * (a * (N * (b * N))) by GROUP_3:13
.= (((a ") * N) * ((b ") * N)) * ((a * N) * (b * N)) by GROUP_3:10 ;
S * T = (a * N) * (b * N) by A8, A6, Def3;
then [.S,T.] = (((a ") * N) * ((b ") * N)) * ((a * N) * (b * N)) by A9, A5, Def3;
hence [.S,T.] = 1_ (G ./. N) by A10, Th24; :: thesis: verum

end;

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