for L being non empty reflexive transitive RelStr st [#] L is directed holds
Tails L is basis of (Tails_Filter L)