let X be non empty set ; :: thesis: 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
let L be non empty reflexive transitive RelStr ; :: thesis: 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
let f be Function of ([#] L),X; :: thesis: 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
let x be Subset of X; :: thesis: ( [#] L is directed & x in f .: (# (Tails L)) implies ex j being Element of L st
for i being Element of L st i >= j holds
f . i in x )
assume that
[#] L is directed and
A2: x in f .: (# (Tails L)) ; :: thesis: ex j being Element of L st
for i being Element of L st i >= j holds
f . i in x
reconsider x0 = x as Subset of X ;
consider b0 being Subset of ([#] L) such that
A3: b0 in # (Tails L) and
A4: x0 = f .: b0 by A2, FUNCT_2:def 10;
consider i being Element of L such that
A5: b0 = uparrow i by A3;

now :: thesis: for j being Element of L st j >= i holds
f . j in x

let j be Element of L; :: thesis: ( j >= i implies f . j in x )
assume j >= i ; :: thesis: f . j in x
then C1: ( i <= j & i in {i} ) by TARSKI:def 1;
j in [#] L ;
then ( j in uparrow i & j in dom f ) by C1, WAYBEL_0:def 16, FUNCT_2:def 1;
hence f . j in x by A4, A5, FUNCT_1:def 6; :: thesis: verum

end;

hence ex j being Element of L st
for i being Element of L st i >= j holds
f . i in x ; :: thesis: verum