let G be Group; :: thesis: for N1, N2 being normal Subgroup of G holds [.N1,N2.] = [.N2,N1.]
let N1, N2 be normal Subgroup of G; :: thesis: [.N1,N2.] = [.N2,N1.]
( [.N1,N2.] is Subgroup of [.N2,N1.] & [.N2,N1.] is Subgroup of [.N1,N2.] ) by Lm2;
hence [.N1,N2.] = [.N2,N1.] by GROUP_2:55; :: thesis: verum