set N = L +id ;
thus L +id is monotone :: thesis: L +id is eventually-directed

proof

A1: netmap (L +id ),L = id L by Def5;
RelStr(# the carrier of (L +id ),the InternalRel of (L +id ) #) = RelStr(# the carrier of L,the InternalRel of L #) by Def5;
hence netmap (L +id ),L is monotone by A1, Th1; :: according to WAYBEL_0:def 9 :: thesis: verum

end;

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 A2: j <= k ; :: thesis: (L +id ) . i <= (L +id ) . k
A3: 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 A3, TMAP_1:91;
hence (L +id ) . i <= (L +id ) . k by A2, A3, YELLOW_0:1; :: thesis: verum

end;

hence L +id is eventually-directed by WAYBEL_0:11; :: thesis: verum