:: deftheorem defines misses MEMBERED:def 20 :
for X, Y being ext-real-membered set holds
( X misses Y iff for e being ExtReal holds
( not e in X or not e in Y ) );