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