let S be Signature; :: thesis: S is Extension of S
thus S is Subsignature of S by INSTALG1:15; :: according to ALGSPEC1:def 5 :: thesis: verum