theorem :: XBOOLE_1:75

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