theorem Th8: :: COHSP_1:8

for X being non empty set st ( 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 ) ) holds
X is c=filtered