:: deftheorem defines meets MEMBERED:def 23 :
for X, Y being integer-membered set holds
( not X meets Y iff for i being Integer holds
( not i in X or not i in Y ) );