:: deftheorem Def11 defines finite STRUCT_0:def 11 :
for S being 1-sorted holds
( S is finite iff the carrier of S is finite );