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