take {{}} ; :: thesis: ( {{}} is c=directed & {{}} is c=filtered & {{}} is finite )
thus ( {{}} is c=directed & {{}} is c=filtered & {{}} is finite ) by Th9; :: thesis: verum