let L be non empty reflexive RelStr ; :: thesis: for D being non empty directed Subset of L

for n being Function of D, the carrier of L

for N being prenet of L st n = id D & N = NetStr(# D,( the InternalRel of L |_2 D),n #) holds

N is eventually-directed

let D be non empty directed Subset of L; :: thesis: for n being Function of D, the carrier of L

for N being prenet of L st n = id D & N = NetStr(# D,( the InternalRel of L |_2 D),n #) holds

N is eventually-directed

let n be Function of D, the carrier of L; :: thesis: for N being prenet of L st n = id D & N = NetStr(# D,( the InternalRel of L |_2 D),n #) holds

N is eventually-directed

let N be prenet of L; :: thesis: ( n = id D & N = NetStr(# D,( the InternalRel of L |_2 D),n #) implies N is eventually-directed )

assume that

A1: n = id D and

A2: N = NetStr(# D,( the InternalRel of L |_2 D),n #) ; :: thesis: N is eventually-directed

for i being Element of N ex j being Element of N st

for k being Element of N st j <= k holds

N . i <= N . k

for n being Function of D, the carrier of L

for N being prenet of L st n = id D & N = NetStr(# D,( the InternalRel of L |_2 D),n #) holds

N is eventually-directed

let D be non empty directed Subset of L; :: thesis: for n being Function of D, the carrier of L

for N being prenet of L st n = id D & N = NetStr(# D,( the InternalRel of L |_2 D),n #) holds

N is eventually-directed

let n be Function of D, the carrier of L; :: thesis: for N being prenet of L st n = id D & N = NetStr(# D,( the InternalRel of L |_2 D),n #) holds

N is eventually-directed

let N be prenet of L; :: thesis: ( n = id D & N = NetStr(# D,( the InternalRel of L |_2 D),n #) implies N is eventually-directed )

assume that

A1: n = id D and

A2: N = NetStr(# D,( the InternalRel of L |_2 D),n #) ; :: thesis: N is eventually-directed

for i being Element of N ex j being Element of N st

for k being Element of N st j <= k holds

N . i <= N . k

proof

hence
N is eventually-directed
by WAYBEL_0:11; :: thesis: verum
let i be Element of N; :: thesis: ex j being Element of N st

for k being Element of N st j <= k holds

N . i <= N . k

take j = i; :: thesis: for k being Element of N st j <= k holds

N . i <= N . k

let k be Element of N; :: thesis: ( j <= k implies N . i <= N . k )

assume A3: j <= k ; :: thesis: N . i <= N . k

the InternalRel of N c= the InternalRel of L by A2, XBOOLE_1:17;

then A4: N is SubRelStr of L by A2, YELLOW_0:def 13;

reconsider nj = n . j, nk = n . k as Element of L by A2, FUNCT_2:5;

( nj = j & nk = k ) by A1, A2;

hence N . i <= N . k by A2, A3, A4, YELLOW_0:59; :: thesis: verum

end;for k being Element of N st j <= k holds

N . i <= N . k

take j = i; :: thesis: for k being Element of N st j <= k holds

N . i <= N . k

let k be Element of N; :: thesis: ( j <= k implies N . i <= N . k )

assume A3: j <= k ; :: thesis: N . i <= N . k

the InternalRel of N c= the InternalRel of L by A2, XBOOLE_1:17;

then A4: N is SubRelStr of L by A2, YELLOW_0:def 13;

reconsider nj = n . j, nk = n . k as Element of L by A2, FUNCT_2:5;

( nj = j & nk = k ) by A1, A2;

hence N . i <= N . k by A2, A3, A4, YELLOW_0:59; :: thesis: verum