:: deftheorem defines {}. SETWISEO:def 1 :
for X being set holds {}. X = {} ;