:: deftheorem Def2 defines void SCMYCIEL:def 2 :
for X being set holds
( X is void iff X = {{}} );