let G be Group; :: thesis: for A, B, C, D being Subset of G st A c= B & C c= D holds

commutators (A,C) c= commutators (B,D)

let A, B, C, D be Subset of G; :: thesis: ( A c= B & C c= D implies commutators (A,C) c= commutators (B,D) )

assume A1: ( A c= B & C c= D ) ; :: thesis: commutators (A,C) c= commutators (B,D)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in commutators (A,C) or x in commutators (B,D) )

assume x in commutators (A,C) ; :: thesis: x in commutators (B,D)

then ex a, c being Element of G st

( x = [.a,c.] & a in A & c in C ) ;

hence x in commutators (B,D) by A1; :: thesis: verum

commutators (A,C) c= commutators (B,D)

let A, B, C, D be Subset of G; :: thesis: ( A c= B & C c= D implies commutators (A,C) c= commutators (B,D) )

assume A1: ( A c= B & C c= D ) ; :: thesis: commutators (A,C) c= commutators (B,D)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in commutators (A,C) or x in commutators (B,D) )

assume x in commutators (A,C) ; :: thesis: x in commutators (B,D)

then ex a, c being Element of G st

( x = [.a,c.] & a in A & c in C ) ;

hence x in commutators (B,D) by A1; :: thesis: verum