let L be non empty reflexive RelStr ; :: thesis: for D being non empty directed Subset of
for n being Function of D,the carrier of L
for N being prenet of 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 ; :: thesis: for n being Function of D,the carrier of L
for N being prenet of 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 st n = id D & N = NetStr(# D,(the InternalRel of L |_2 D),n #) holds
N is eventually-directed
let N be prenet of ; :: 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 ex j being Element of st
for k being Element of st j <= k holds
N . i <= N . k

proof

let i be Element of ; :: thesis: ex j being Element of st
for k being Element of st j <= k holds
N . i <= N . k
take j = i; :: thesis: for k being Element of st j <= k holds
N . i <= N . k
let k be Element of ; :: 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 by A2, FUNCT_2:7;
( 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