let G be Group; :: thesis: G ` is characteristic
A1: [.(1_ G),(1_ G).] in commutators G ;
for phi being Automorphism of G holds phi .: (commutators G) = commutators G by Th43;
hence G ` is characteristic by A1, Th45; :: thesis: verum