let L be transitive antisymmetric with_infima RelStr ; :: thesis: for N being prenet of L
for x being Element of L st N is eventually-directed holds
x "/\" N is eventually-directed
let N be prenet of L; :: thesis: for x being Element of L st N is eventually-directed holds
x "/\" N is eventually-directed
let x be Element of L; :: thesis: ( N is eventually-directed implies x "/\" N is eventually-directed )
assume A1: N is eventually-directed ; :: thesis: x "/\" N is eventually-directed
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: ex j being Element of (x "/\" N) st
for k being Element of (x "/\" N) st j <= k holds
(x "/\" N) . i1 <= (x "/\" N) . k
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: for k being Element of (x "/\" N) st j1 <= k holds
(x "/\" N) . i1 <= (x "/\" N) . k
let k1 be Element of (x "/\" N); :: thesis: ( j1 <= k1 implies (x "/\" N) . i1 <= (x "/\" N) . k1 )
reconsider k = k1 as Element of N by Th22;
assume j1 <= k1 ; :: thesis: (x "/\" N) . i1 <= (x "/\" N) . k1
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: verum

end;

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