let G be Group; 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; ( A c= B & C c= D implies commutators (A,C) c= commutators (B,D) )
assume A1:
( A c= B & C c= D )
; commutators (A,C) c= commutators (B,D)
let x be object ; TARSKI:def 3 ( not x in commutators (A,C) or x in commutators (B,D) )
assume
x in commutators (A,C)
; 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; verum