let A, B be Subgroup of G; :: thesis: [.A,B.] = [.B,A.]
( [.A,B.] is Subgroup of [.B,A.] & [.B,A.] is Subgroup of [.A,B.] ) by Th9;
hence [.A,B.] = [.B,A.] by GROUP_2:55; :: thesis: verum