theorem :: COHSP_1:7

for X being set st X is c=filtered holds
for a, b being set st a in X & b in X holds
ex c being set st
( c c= a /\ b & c in X )