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