theorem Th15: :: INSTALG1:15

for S being feasible ManySortedSign holds S is Subsignature of S