for X, Y being set st X meets Y holds
X /\ Y meets Y