let S be empty 1-sorted ; :: thesis: S is finite
thus the carrier of S is finite ; :: according to STRUCT_0:def 11 :: thesis: verum