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 )

G is commutative

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 A2:
for a, b being Element of G holds [.a,b.] = 1_ G
; :: thesis: G is commutative Group
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;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

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.] = 1_ G by A2;

hence a * b = b * a by Th36; :: thesis: verum

end;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