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

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