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 set ; :: 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 consider a, c being Element of G such that
A2: x = [.a,c.] and
A3: ( a in A & c in C ) ;
thus x in commutators B,D by A1, A2, A3; :: thesis: verum