let G be Group; :: thesis: for A, B being Subgroup of G holds [.A,B.] = [.B,A.]
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:64; :: thesis: verum