take {} L ; :: thesis: ( {} L is directed & {} L is filtered )
thus ( {} L is directed & {} L is filtered ) ; :: thesis: verum