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