let S1 be Signature; :: thesis: for S2 being Extension of S1
for S3 being Extension of S2 holds S3 is Extension of S1
let S2 be Extension of S1; :: thesis: for S3 being Extension of S2 holds S3 is Extension of S1
let S3 be Extension of S2; :: thesis: S3 is Extension of S1
A1: S2 is Subsignature of S3 by Def5;
S1 is Subsignature of S2 by Def5;
then S1 is Subsignature of S3 by A1, INSTALG1:16;
hence S3 is Extension of S1 by Def5; :: thesis: verum