:: deftheorem defines {} XBOOLE_0:def 2 :
{} = the empty set ;