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}

proof

let x be set ; :: 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;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {[.a,b.]} or x in commutators {a},{b} )
assume x in {[.a,b.]} ; :: thesis: x in commutators {a},{b}
then ( x = [.a,b.] & a in {a} & b in {b} ) by TARSKI:def 1;
hence x in commutators {a},{b} ; :: thesis: verum