:: deftheorem DefL9 defines Tails_Filter CARDFIL2:def 15 :
for L being non empty reflexive transitive RelStr st [#] L is directed holds
Tails_Filter L = <.(Tails L).];