let G be Group; :: thesis: for B, A being Subgroup of G st B is Subgroup of A holds
[.A,B.] is Subgroup of A
let B, A 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 Th11;
then [.A,B.] is Subgroup of gr (carr A) by GROUP_4:41;
hence [.A,B.] is Subgroup of A by A1, GROUP_2:65; :: thesis: verum