:: deftheorem Def4 defines void PENCIL_1:def 4 :
for S being TopStruct holds
( S is void iff the topology of S is empty );