let G be Group; for a, b being Element of G
for A, B being Subset of G st a in A & b in B holds
[.a,b.] in [.A,B.]
let a, b be Element of G; for A, B being Subset of G st a in A & b in B holds
[.a,b.] in [.A,B.]
let A, B be Subset of G; ( a in A & b in B implies [.a,b.] in [.A,B.] )
assume
( a in A & b in B )
; [.a,b.] in [.A,B.]
then
[.a,b.] in commutators (A,B)
;
hence
[.a,b.] in [.A,B.]
by GROUP_4:29; verum