for N being antisymmetric with_infima RelStr
for D, E being Subset of N
for X being upper Subset of N st D misses X holds
D "/\" E misses X