theorem Th9: :: COHSP_1:9

for x being set holds
( {x} is c=directed & {x} is c=filtered )