theorem Th14: :: CARDFIL2:41

for L being non empty reflexive transitive RelStr st [#] L is directed holds
<.(Tails L).] is Filter of [#] L