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 b1 being Element of the carrier of G holds a * b1 = b1 * 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