let G be strict Group; :: thesis: InnAut G c= Aut G

now

let q be set ; :: thesis: ( q in InnAut G implies 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 Th13;
hence q in Aut G by A1; :: thesis: verum

end;

hence InnAut G c= Aut G by TARSKI:def 3; :: thesis: verum