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