set N = L +id ;
( netmap ((L +id),L) = id L & RelStr(# the carrier of (L +id), the InternalRel of (L +id) #) = RelStr(# the carrier of L, the InternalRel of L #) ) by Def5;
then netmap ((L +id),L) is monotone by Th1;
hence L +id is monotone ; :: thesis: L +id is eventually-directed
for i being Element of (L +id) ex j being Element of (L +id) st
for k being Element of (L +id) st j <= k holds
(L +id) . i <= (L +id) . k
proof
let i be Element of (L +id); :: thesis: ex j being Element of (L +id) st
for k being Element of (L +id) st j <= k holds
(L +id) . i <= (L +id) . k
take j = i; :: thesis: for k being Element of (L +id) st j <= k holds
(L +id) . i <= (L +id) . k
let k be Element of (L +id); :: thesis: ( j <= k implies (L +id) . i <= (L +id) . k )
assume A1: j <= k ; :: thesis: (L +id) . i <= (L +id) . k
A2: RelStr(# the carrier of (L +id), the InternalRel of (L +id) #) = RelStr(# the carrier of L, the InternalRel of L #) by Def5;
the mapping of (L +id) = id L by Def5;
then ( the mapping of (L +id) . i = i & the mapping of (L +id) . k = k ) by A2;
hence (L +id) . i <= (L +id) . k by A1, A2; :: thesis: verum
end;
hence L +id is eventually-directed by WAYBEL_0:11; :: thesis: verum