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