let G be Group; :: thesis: InnAut G c= Aut G
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in InnAut G or q in Aut G )
assume q in InnAut G ; :: thesis: q in Aut G
then consider f being Element of InnAut G such that
A1: f = q ;
f is Element of Aut G by Th12;
hence q in Aut G by A1; :: thesis: verum