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
( S1 is Subsignature of S2 & S2 is Subsignature of S3 ) by Def5;
then S1 is Subsignature of S3 by INSTALG1:17;
hence S3 is Extension of S1 by Def5; :: thesis: verum