let G be Group; :: thesis: for H, K being strict characteristic Subgroup of G holds [.H,K.] is characteristic Subgroup of G
let H, K be strict characteristic Subgroup of G; :: thesis: [.H,K.] is characteristic Subgroup of G
set A = commutators (H,K);
reconsider A = commutators (H,K) as non empty Subset of G by GROUP_5:53;
for phi being Automorphism of G holds phi .: A = A by Th53;
hence [.H,K.] is characteristic Subgroup of G by Th45; :: thesis: verum