:: deftheorem Def7 defines segmental MSUALG_1:def 7 :
for IT being ManySortedSign holds
( IT is segmental iff ex n being Nat st the carrier' of IT = Seg n );