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