for X being non empty set
for F1, F2, F being Filter of X st F is_filter-finer_than F1 & F is_filter-finer_than F2 holds
for M1 being Element of F1
for M2 being Element of F2 holds not M1 /\ M2 is empty