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
reconsider nj = n . j, nk = n . k as Element of L by A2, FUNCT_2:7;
A4: N is SubRelStr of L

proof

thus the carrier of N c= the carrier of L by A2; :: according to YELLOW_0:def 13 :: thesis: the InternalRel of N c= the InternalRel of L
thus the InternalRel of N c= the InternalRel of L by A2, XBOOLE_1:17; :: thesis: verum

end;

( nj = j & nk = k ) by A1, A2, FUNCT_1:35;
hence N . i <= N . k by A2, A3, A4, YELLOW_0:60; :: thesis: verum

end;

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