let L be transitive antisymmetric with_infima RelStr ; :: thesis:
let N be prenet of L; :: thesis:
let x be Element of L; :: thesis:
assume A1: N is eventually-directed ; :: thesis:
A2: RelStr(# the carrier of (x "/\" N), the InternalRel of (x "/\" N) #) = RelStr(# the carrier of N, the InternalRel of N #) by Def3;
for i being Element of (x "/\" N) ex j being Element of (x "/\" N) st
for k being Element of (x "/\" N) st j <= k holds
(x "/\" N) . i <= (x "/\" N) . k

proof

let i1 be Element of (x "/\" N); :: thesis:
reconsider i = i1 as Element of N by Th22;
consider j being Element of N such that
A3: for k being Element of N st j <= k holds
N . i <= N . k by A1, WAYBEL_0:11;
reconsider j1 = j as Element of (x "/\" N) by Th22;
take j1 ; :: thesis:
let k1 be Element of (x "/\" N); :: thesis:
reconsider k = k1 as Element of N by Th22;
assume j1 <= k1 ; :: thesis:
then j <= k by A2, YELLOW_0:1;
then A4: N . i <= N . k by A3;
( ex yi being Element of L st
( yi = the mapping of N . i1 & the mapping of (x "/\" N) . i1 = x "/\" yi ) & ex yk being Element of L st
( yk = the mapping of N . k1 & the mapping of (x "/\" N) . k1 = x "/\" yk ) ) by Def3;
hence (x "/\" N) . i1 <= (x "/\" N) . k1 by A4, WAYBEL_1:1; :: thesis:

end;

hence x "/\" N is eventually-directed by WAYBEL_0:11; :: thesis: