theorem Th9: :: GRNILP_1:9

for G being Group
for A, B being Subgroup of G holds [.A,B.] is Subgroup of [.B,A.]