let G be Group; :: thesis: ( G is commutative Group iff for a, b being Element of G holds [.a,b.] = 1_ G )
thus ( G is commutative Group implies for a, b being Element of G holds [.a,b.] = 1_ G ) :: thesis: ( ( for a, b being Element of G holds [.a,b.] = 1_ G ) implies G is commutative Group )

proof

assume A1: G is commutative Group ; :: thesis: for a, b being Element of G holds [.a,b.] = 1_ G
let a, b be Element of G; :: thesis: [.a,b.] = 1_ G
a * b = b * a by A1, Lm1;
hence [.a,b.] = 1_ G by Th36; :: thesis: verum

end;

assume A2: for a, b being Element of G holds [.a,b.] = 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.] = 1_ G by A2;
hence a * b = b * a by Th36; :: thesis: verum

end;

hence G is commutative Group ; :: thesis: verum