:: deftheorem Def1 defines feasible INSTALG1:def 1 :
for S being ManySortedSign holds
( S is feasible iff ( the carrier of S = {} implies the carrier' of S = {} ) );