let G be Group; :: thesis: for a, b being Element of
for A, B being Subset of st a in A & b in B holds
[.a,b.] in [.A,B.]
let a, b be Element of ; :: thesis: for A, B being Subset of st a in A & b in B holds
[.a,b.] in [.A,B.]
let A, B be Subset of ; :: 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:38; :: thesis: verum