let S be 1-sorted ; :: thesis: ( S is trivial implies S is finite )
assume S is trivial ; :: thesis: S is finite
then reconsider C = the carrier of S as trivial set ;
C is finite ;
hence the carrier of S is finite ; :: according to STRUCT_0:def 11 :: thesis: verum