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:
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
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 ;
then A4: N is SubRelStr of L by ;
reconsider nj = n . j, nk = n . k as Element of L by ;
( nj = j & nk = k ) by A1, A2;
hence N . i <= N . k by ; :: thesis: verum
end;
hence N is eventually-directed by WAYBEL_0:11; :: thesis: verum