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