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

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 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;

hence N is eventually-directed by WAYBEL_0:11; :: thesis: verum