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