let G be Group; :: thesis: for A, B being Subgroup of G st B is Subgroup of A holds
[.A,B.] is Subgroup of A
let A, B be Subgroup of G; :: thesis: ( B is Subgroup of A implies [.A,B.] is Subgroup of A )
A1: gr (carr A) is Subgroup of A by Lm1;
assume B is Subgroup of A ; :: thesis: [.A,B.] is Subgroup of A
then commutators (A,B) c= carr A by Th10;
then [.A,B.] is Subgroup of gr (carr A) by GROUP_4:32;
hence [.A,B.] is Subgroup of A by A1, GROUP_2:56; :: thesis: verum