for X being non empty set
for L being non empty reflexive transitive RelStr
for f being Function of ([#] L),X
for x being Subset of X st [#] L is directed & x in f .: (# (Tails L)) holds
ex j being Element of L st
for i being Element of L st i >= j holds
f . i in x