let G be Group; :: thesis: for A being Subset of G holds
( commutators ({} the carrier of G),A = {} & commutators A,({} the carrier of G) = {} )
let A be Subset of G; :: thesis: ( commutators ({} the carrier of G),A = {} & commutators A,({} the carrier of G) = {} )
commutators ({} the carrier of G),A c= {}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in commutators ({} the carrier of G),A or x in {} )
assume x in commutators ({} the carrier of G),A ; :: thesis: x in {}
then ex a, b being Element of G st
( x = [.a,b.] & a in {} the carrier of G & b in A ) ;
hence x in {} ; :: thesis: verum

end;

hence commutators ({} the carrier of G),A = {} ; :: thesis: commutators A,({} the carrier of G) = {}
thus commutators A,({} the carrier of G) c= {} :: according to XBOOLE_0:def 10 :: thesis: {} c= commutators A,({} the carrier of G)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in commutators A,({} the carrier of G) or x in {} )
assume x in commutators A,({} the carrier of G) ; :: thesis: x in {}
then ex a, b being Element of G st
( x = [.a,b.] & a in A & b in {} the carrier of G ) ;
hence x in {} ; :: thesis: verum

end;

thus {} c= commutators A,({} the carrier of G) by XBOOLE_1:2; :: thesis: verum