theorem Th15: :: CARDFIL2:42

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