let S be 2-sorted ; :: thesis: ( S is void implies S is feasible )
assume the carrier' of S is empty ; :: according to STRUCT_0:def 13 :: thesis: S is feasible
hence S is feasible by Def20; :: thesis: verum