let G be Group; :: thesis: for a, b being Element of G holds commutators ({a},{b}) = {[.a,b.]}

let a, b be Element of G; :: thesis: commutators ({a},{b}) = {[.a,b.]}

thus commutators ({a},{b}) c= {[.a,b.]} :: according to XBOOLE_0:def 10 :: thesis: {[.a,b.]} c= commutators ({a},{b})

assume x in {[.a,b.]} ; :: thesis: x in commutators ({a},{b})

then A3: x = [.a,b.] by TARSKI:def 1;

( a in {a} & b in {b} ) by TARSKI:def 1;

hence x in commutators ({a},{b}) by A3; :: thesis: verum

let a, b be Element of G; :: thesis: commutators ({a},{b}) = {[.a,b.]}

thus commutators ({a},{b}) c= {[.a,b.]} :: according to XBOOLE_0:def 10 :: thesis: {[.a,b.]} c= commutators ({a},{b})

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {[.a,b.]} or x in commutators ({a},{b}) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in commutators ({a},{b}) or x in {[.a,b.]} )

assume x in commutators ({a},{b}) ; :: thesis: x in {[.a,b.]}

then consider c, d being Element of G such that

A1: x = [.c,d.] and

A2: ( c in {a} & d in {b} ) ;

( c = a & b = d ) by A2, TARSKI:def 1;

hence x in {[.a,b.]} by A1, TARSKI:def 1; :: thesis: verum

end;assume x in commutators ({a},{b}) ; :: thesis: x in {[.a,b.]}

then consider c, d being Element of G such that

A1: x = [.c,d.] and

A2: ( c in {a} & d in {b} ) ;

( c = a & b = d ) by A2, TARSKI:def 1;

hence x in {[.a,b.]} by A1, TARSKI:def 1; :: thesis: verum

assume x in {[.a,b.]} ; :: thesis: x in commutators ({a},{b})

then A3: x = [.a,b.] by TARSKI:def 1;

( a in {a} & b in {b} ) by TARSKI:def 1;

hence x in commutators ({a},{b}) by A3; :: thesis: verum