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) = {} )
thus commutators ({} the carrier of G),A = {} :: thesis: commutators A,({} the carrier of G) = {}

proof

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

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 consider a, b being Element of G such that
x = [.a,b.] and
A1: a in {} the carrier of G and
b in A ;
thus x in {} by A1; :: thesis: verum

end;

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

end;

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 consider a, b being Element of G such that
( x = [.a,b.] & a in A ) and
A2: b in {} the carrier of G ;
thus x in {} by A2; :: thesis: verum

end;

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