let G be Group; :: thesis: 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; :: thesis: 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; :: thesis: ( a in A & b in B implies [.a,b.] in [.A,B.] )
assume ( a in A & b in B ) ; :: thesis: [.a,b.] in [.A,B.]
then [.a,b.] in commutators (A,B) ;
hence [.a,b.] in [.A,B.] by GROUP_4:29; :: thesis: verum