:: deftheorem Def2 defines inner GROUP_22:def 3 :
for G being Group
for IT being Automorphism of G holds
( IT is inner iff ex a being Element of G st a is_inner_wrt IT );