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;
( S " = @ (S " ) & T " = @ (T " ) & S " = (a " ) * N & T " = (b " ) * N ) by Th30;
then A2: (S " ) * (T " ) = ((a " ) * N) * ((b " ) * N) by Def4;
A3: S * T = (a * N) * (b * N) by Def4;
[.S,T.] = ((S " ) * (T " )) * (S * T) by GROUP_5:19;
then ( [.S,T.] = (((a " ) * N) * ((b " ) * N)) * ((a * N) * (b * N)) & [.S,T.] = 1_ (G ./. N) & 1_ (G ./. N) = carr N ) by A1, A2, A3, Def4, Th29, GROUP_5:40;
then carr N = (((a " ) * N) * ((b " ) * N)) * (a * (N * (b * N))) by 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)
consider a being Element of G such that
A5: ( S = a * N & S = N * a ) by Th15;
consider b being Element of G such that
A6: ( T = b * N & T = N * b ) by Th15;
[.a,b.] in N by A4, Th8;
then A7: 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 " = @ (S " ) & T " = @ (T " ) & S " = (a " ) * N & T " = (b " ) * N ) by A5, A6, Th30;
then A8: (S " ) * (T " ) = ((a " ) * N) * ((b " ) * N) by Def4;
A9: S * T = (a * N) * (b * N) by A5, A6, Def4;
[.S,T.] = ((S " ) * (T " )) * (S * T) by GROUP_5:19;
then ( [.S,T.] = (((a " ) * N) * ((b " ) * N)) * ((a * N) * (b * N)) & 1_ (G ./. N) = carr N ) by A8, A9, Def4, Th29;
hence [.S,T.] = 1_ (G ./. N) by A7; :: thesis: verum

end;

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