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