let L be non empty reflexive transitive RelStr ; :: thesis: ( [#] L is directed implies Tails L is basis of (Tails_Filter L) )
assume [#] L is directed ; :: thesis: Tails L is basis of (Tails_Filter L)
then Tails_Filter L = <.(Tails L).] by DefL9;
hence Tails L is basis of (Tails_Filter L) by Th07; :: thesis: verum