:: deftheorem Def13 defines void STRUCT_0:def 13 :
for S being 2-sorted holds
( S is void iff the carrier' of S is empty );