take S ; :: thesis: S is Subsignature of S
thus S is Subsignature of S by INSTALG1:16; :: thesis: verum