consider x being Element of C;
( {x} is Subset of C & {x} is c=directed & {x} is c=filtered & {x} is finite ) by Th9, ZFMISC_1:37;
hence ex b₁ being Subset of C st
( b₁ is c=directed & b₁ is c=filtered & b₁ is finite ) ; :: thesis: verum