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= {}

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

( 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

hence
commutators (({} the carrier of G),A) = {}
; :: thesis: commutators (A,({} the carrier of G)) = {}
let x be object ; :: 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;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

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

proof

thus
{} c= commutators (A,({} the carrier of G))
; :: thesis: verum
let x be object ; :: 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;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