let S be 1-sorted ; :: thesis: ( not S is empty & S is trivial implies S is 1 -element )
assume A: not the carrier of S is empty ; :: according to STRUCT_0:def 1 :: thesis: ( not S is trivial or S is 1 -element )
assume S is trivial ; :: thesis: S is 1 -element
hence the carrier of S is 1 -element by A; :: according to STRUCT_0:def 19 :: thesis: verum