let S be ManySortedSign ; :: thesis: ( S is void implies S is feasible )
assume that
A1: S is void and
the carrier of S = {} ; :: according to INSTALG1:def 1 :: thesis: the carrier' of S = {}
thus the carrier' of S = {} by A1; :: thesis: verum