:: deftheorem defines misses XBOOLE_0:def 7 :
for X, Y being set holds
( X misses Y iff X /\ Y = {} );