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

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

hence
x "/\" N is eventually-directed
by WAYBEL_0:11; :: thesis: verum
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;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