for L being non empty 1-sorted
for N being net of L
for X, Y being set st N is_eventually_in X & N is_eventually_in Y holds
X meets Y