:: deftheorem Def5 defines InnAutGroup AUTGROUP:def 5 :
for G being strict Group
for b₂ being strict normal Subgroup of AutGroup G holds
( b₂ = InnAutGroup G iff the carrier of b₂ = InnAut G );