let S be 1-sorted ; :: thesis: ( S is empty implies S is trivial )
assume the carrier of S is empty ; :: according to STRUCT_0:def 1 :: thesis: S is trivial
hence the carrier of S is trivial ; :: according to STRUCT_0:def 9 :: thesis: verum