let G be Group; :: thesis: ( G is commutative Group iff commutators G = {(1_ G)} )
thus ( G is commutative Group implies commutators G = {(1_ G)} ) by Th57; :: thesis: ( commutators G = {(1_ G)} implies G is commutative Group )
assume A1: commutators G = {(1_ G)} ; :: thesis: G is commutative Group
G is commutative

proof

let a be Element of G; :: according to GROUP_1:def 12 :: thesis: for b₁ being Element of the carrier of G holds a * b₁ = b₁ * a
let b be Element of G; :: thesis: a * b = b * a
[.a,b.] in {(1_ G)} by A1;
then [.a,b.] = 1_ G by TARSKI:def 1;
hence a * b = b * a by Th36; :: thesis: verum

end;

hence G is commutative Group ; :: thesis: verum