theorem :: GRNILP_1:12
for G being Group
for A, B being Subgroup of G st B is Subgroup of A holds
[.B,A.] is Subgroup of A by Th11;