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