let G be Group; :: thesis: ( G is commutative Group iff for A, B being Subset of G st A <> {} & B <> {} holds
commutators A,B = {(1_ G)} )
thus ( G is commutative Group implies for A, B being Subset of G st A <> {} & B <> {} holds
commutators A,B = {(1_ G)} ) :: thesis: ( ( for A, B being Subset of G st A <> {} & B <> {} holds
commutators A,B = {(1_ G)} ) implies G is commutative Group )

proof

assume A1: G is commutative Group ; :: thesis: for A, B being Subset of G st A <> {} & B <> {} holds
commutators A,B = {(1_ G)}
let A, B be Subset of G; :: thesis: ( A <> {} & B <> {} implies commutators A,B = {(1_ G)} )
assume A2: ( A <> {} & B <> {} ) ; :: thesis: commutators A,B = {(1_ G)}
thus commutators A,B c= {(1_ G)} :: according to XBOOLE_0:def 10 :: thesis: {(1_ G)} c= commutators A,B

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in commutators A,B or x in {(1_ G)} )
assume x in commutators A,B ; :: thesis: x in {(1_ G)}
then consider a, b being Element of G such that
A3: x = [.a,b.] and
a in A and
b in B ;
x = ((a " ) * ((b " ) * a)) * b by A3, Th19
.= ((a " ) * (a * (b " ))) * b by A1, Lm1
.= (b " ) * b by GROUP_3:1
.= 1_ G by GROUP_1:def 6 ;
hence x in {(1_ G)} by TARSKI:def 1; :: thesis: verum

end;

consider b being Element of B;
consider a being Element of A;
reconsider a = a, b = b as Element of G by A2, TARSKI:def 3;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(1_ G)} or x in commutators A,B )
assume x in {(1_ G)} ; :: thesis: x in commutators A,B
then A4: x = 1_ G by TARSKI:def 1;
[.a,b.] = ((a " ) * ((b " ) * a)) * b by Th19
.= ((a " ) * (a * (b " ))) * b by A1, Lm1
.= (b " ) * b by GROUP_3:1
.= x by A4, GROUP_1:def 6 ;
hence x in commutators A,B by A2; :: thesis: verum

end;

assume A5: for A, B being Subset of G st A <> {} & B <> {} holds
commutators A,B = {(1_ G)} ; :: thesis: G is commutative Group
G is commutative

proof

let a be Element of G; :: according to GROUP_1:def 16 :: 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 in {a} & b in {b} ) by TARSKI:def 1;
then A6: [.a,b.] in commutators {a},{b} ;
commutators {a},{b} = {(1_ G)} by A5;
then [.a,b.] = 1_ G by A6, TARSKI:def 1;
then ((a " ) * (b " )) * (a * b) = 1_ G by Th19;
then ((b * a) " ) * (a * b) = 1_ G by GROUP_1:25;
then a * b = ((b * a) " ) " by GROUP_1:20;
hence a * b = b * a ; :: thesis: verum

end;

hence G is commutative Group ; :: thesis: verum