let L be non empty RelStr ; for N being prenet of L st N is eventually-directed holds
rng (netmap (N,L)) is directed
let N be prenet of L; ( N is eventually-directed implies rng (netmap (N,L)) is directed )
assume A1:
N is eventually-directed
; rng (netmap (N,L)) is directed
set f = netmap (N,L);
let x, y be Element of L; WAYBEL_0:def 1 ( not x in rng (netmap (N,L)) or not y in rng (netmap (N,L)) or ex b1 being Element of the carrier of L st
( b1 in rng (netmap (N,L)) & x <= b1 & y <= b1 ) )
assume that
A2:
x in rng (netmap (N,L))
and
A3:
y in rng (netmap (N,L))
; ex b1 being Element of the carrier of L st
( b1 in rng (netmap (N,L)) & x <= b1 & y <= b1 )
consider a being object such that
A4:
a in dom (netmap (N,L))
and
A5:
(netmap (N,L)) . a = x
by A2, FUNCT_1:def 3;
consider b being object such that
A6:
b in dom (netmap (N,L))
and
A7:
(netmap (N,L)) . b = y
by A3, FUNCT_1:def 3;
reconsider a = a, b = b as Element of N by A4, A6;
consider ja being Element of N such that
A8:
for k being Element of N st ja <= k holds
N . a <= N . k
by A1, WAYBEL_0:11;
consider jb being Element of N such that
A9:
for k being Element of N st jb <= k holds
N . b <= N . k
by A1, WAYBEL_0:11;
[#] N is directed
by WAYBEL_0:def 6;
then consider c being Element of N such that
c in [#] N
and
A10:
( ja <= c & jb <= c )
;
take z = (netmap (N,L)) . c; ( z in rng (netmap (N,L)) & x <= z & y <= z )
dom (netmap (N,L)) = the carrier of N
by FUNCT_2:def 1;
hence
z in rng (netmap (N,L))
by FUNCT_1:def 3; ( x <= z & y <= z )
N . c = (netmap (N,L)) . c
;
hence
( x <= z & y <= z )
by A5, A7, A8, A9, A10; verum