for S being feasible ManySortedSign
for T being Subsignature of S holds
( the carrier of T c= the carrier of S & the carrier' of T c= the carrier' of S )