theorem Th12: :: COHSP_1:12

for X being set holds
( Fin X is c=directed & Fin X is c=filtered )