let S be ManySortedSign ; :: thesis: ( not S is empty implies S is feasible )
assume ( not the carrier of S is empty & the carrier of S = {} ) ; :: according to STRUCT_0:def 1,INSTALG1:def 1 :: thesis: the carrier' of S = {}
hence the carrier' of S = {} ; :: thesis: verum