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 by WAYBEL_0:def 9; :: 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, FUNCT_1:35;
hence (L +id ) . i <= (L +id ) . k by A1, A2, YELLOW_0:1; :: thesis: verum

end;

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