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

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

hence
G is commutative Group
; :: thesis: verum
let a be Element of G; :: according to GROUP_1:def 12 :: thesis: for b_{1} being Element of the carrier of G holds a * b_{1} = b_{1} * 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;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