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