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 & ex j being Element of L st
for i being Element of L st i >= j holds
f . i in x holds
ex b being Element of Tails L st f .: b c= 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 & ex j being Element of L st
for i being Element of L st i >= j holds
f . i in x holds
ex b being Element of Tails L st f .: b c= x
let f be Function of ([#] L),X; :: thesis: for x being Subset of X st [#] L is directed & ex j being Element of L st
for i being Element of L st i >= j holds
f . i in x holds
ex b being Element of Tails L st f .: b c= x
let x be Subset of X; :: thesis: ( [#] L is directed & ex j being Element of L st
for i being Element of L st i >= j holds
f . i in x implies ex b being Element of Tails L st f .: b c= x )
assume that
[#] L is directed and
A1: ex j being Element of L st
for i being Element of L st i >= j holds
f . i in x ; :: thesis: ex b being Element of Tails L st f .: b c= x
consider j0 being Element of L such that
A2: for i being Element of L st i >= j0 holds
f . i in x by A1;
set b0 = uparrow {j0};
uparrow {j0} = uparrow j0 ;
then A3: uparrow {j0} in # (Tails L) ;

now :: thesis: for t being object st t in f .: (uparrow {j0}) holds
t in x

let t be object ; :: thesis: ( t in f .: (uparrow {j0}) implies t in x )
assume t in f .: (uparrow {j0}) ; :: thesis: t in x
then consider x0 being object such that
A4: x0 in dom f and
A5: x0 in uparrow j0 and
A6: t = f . x0 by FUNCT_1:def 6;
reconsider x1 = x0 as Element of L by A4;
consider y1 being Element of L such that
A7: y1 <= x1 and
A8: y1 in {j0} by A5, WAYBEL_0:def 16;
y1 = j0 by A8, TARSKI:def 1;
hence t in x by A2, A6, A7; :: thesis: verum

end;

then f .: (uparrow {j0}) c= x ;
hence ex b being Element of Tails L st f .: b c= x by A3; :: thesis: verum